Home | Metamath
Proof Explorer Theorem List (p. 267 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wksonproplem 26601* | Lemma for theorems for properties of walks between two vertices, e.g. trlsonprop 26604. (Contributed by AV, 16-Jan-2021.) |
Vtx Vtx Vtx Walks | ||
Theorem | trlsonfval 26602* | The set of trails between two vertices. (Contributed by Alexander van der Vekens, 4-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 15-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
Vtx TrailsOn WalksOn Trails | ||
Theorem | istrlson 26603 | Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
Vtx TrailsOn WalksOn Trails | ||
Theorem | trlsonprop 26604 | Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 16-Jan-2021.) |
Vtx TrailsOn WalksOn Trails | ||
Theorem | trlsonistrl 26605 | A trail between two vertices is a trail. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 7-Jan-2021.) |
TrailsOn Trails | ||
Theorem | trlsonwlkon 26606 | A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) |
TrailsOn WalksOn | ||
Theorem | trlontrl 26607 | A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021.) |
Trails TrailsOn | ||
Syntax | cpths 26608 | Extend class notation with paths (of a graph). |
Paths | ||
Syntax | cspths 26609 | Extend class notation with simple paths (of a graph). |
SPaths | ||
Syntax | cpthson 26610 | Extend class notation with paths between two vertices (within a graph). |
PathsOn | ||
Syntax | cspthson 26611 | Extend class notation with simple paths between two vertices (within a graph). |
SPathsOn | ||
Definition | df-pths 26612* |
Define the set of all paths (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." According to Bollobas: "... a path is a walk with distinct vertices.", see Notation of [Bollobas] p. 5. (A walk with distinct vertices is actually a simple path, see upgrwlkdvspth 26635). Therefore, a path can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, which is injective restricted to the set { 1 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
Paths Trails ..^ ..^ | ||
Definition | df-spths 26613* |
Define the set of all simple paths (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." Therefore, a simple path can be represented by an injective mapping f from { 1 , ... , n } and an injective mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the simple path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
SPaths Trails | ||
Definition | df-pthson 26614* | Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
PathsOn Vtx Vtx TrailsOn Paths | ||
Definition | df-spthson 26615* | Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.) |
SPathsOn Vtx Vtx TrailsOn SPaths | ||
Theorem | relpths 26616 | The set Paths of all paths on is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021.) |
Paths | ||
Theorem | pthsfval 26617* | The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
Paths Trails ..^ ..^ | ||
Theorem | spthsfval 26618* | The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
SPaths Trails | ||
Theorem | ispth 26619 | Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
Paths Trails ..^ ..^ | ||
Theorem | isspth 26620 | Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
SPaths Trails | ||
Theorem | pthistrl 26621 | A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Paths Trails | ||
Theorem | spthispth 26622 | A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
SPaths Paths | ||
Theorem | pthiswlk 26623 | A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.) |
Paths Walks | ||
Theorem | spthiswlk 26624 | A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.) |
SPaths Walks | ||
Theorem | pthdivtx 26625 | The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.) |
Paths ..^ | ||
Theorem | pthdadjvtx 26626 | The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.) |
Paths ..^ | ||
Theorem | 2pthnloop 26627* | A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon 27011. (Contributed by AV, 6-Feb-2021.) |
iEdg Paths ..^ | ||
Theorem | upgr2pthnlp 26628* | A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.) |
iEdg UPGraph Paths ..^ | ||
Theorem | spthdifv 26629 | The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 30-Oct-2021.) |
SPaths Vtx | ||
Theorem | spthdep 26630 | A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
SPaths | ||
Theorem | pthdepisspth 26631 | A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 12-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Paths SPaths | ||
Theorem | upgrwlkdvdelem 26632* | Lemma for upgrwlkdvde 26633. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.) |
Word ..^ | ||
Theorem | upgrwlkdvde 26633 | In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 26634. (Contributed by AV, 17-Jan-2021.) |
UPGraph Walks | ||
Theorem | upgrspthswlk 26634* | The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p0, p1, p2 } be a hyperedge, then ( p0, e, p1, e, p2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021.) (Proof shortened by AV, 17-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
UPGraph SPaths Walks | ||
Theorem | upgrwlkdvspth 26635 | A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 26634. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.) |
UPGraph Walks SPaths | ||
Theorem | pthsonfval 26636* | The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
Vtx PathsOn TrailsOn Paths | ||
Theorem | spthson 26637* | The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
Vtx SPathsOn TrailsOn SPaths | ||
Theorem | ispthson 26638 | Properties of a pair of functions to be a path between two given vertices. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
Vtx PathsOn TrailsOn Paths | ||
Theorem | isspthson 26639 | Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
Vtx SPathsOn TrailsOn SPaths | ||
Theorem | pthsonprop 26640 | Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.) |
Vtx PathsOn TrailsOn Paths | ||
Theorem | spthonprop 26641 | Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) |
Vtx SPathsOn TrailsOn SPaths | ||
Theorem | pthonispth 26642 | A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 17-Jan-2021.) |
PathsOn Paths | ||
Theorem | pthontrlon 26643 | A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.) |
PathsOn TrailsOn | ||
Theorem | pthonpth 26644 | A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.) |
Paths PathsOn | ||
Theorem | isspthonpth 26645 | A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-Jan-2021.) |
Vtx SPathsOn SPaths | ||
Theorem | spthonisspth 26646 | A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 18-Jan-2021.) |
SPathsOn SPaths | ||
Theorem | spthonpthon 26647 | A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.) |
SPathsOn PathsOn | ||
Theorem | spthonepeq 26648 | The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 18-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
SPathsOn | ||
Theorem | uhgrwkspthlem1 26649 | Lemma 1 for uhgrwkspth 26651. (Contributed by AV, 25-Jan-2021.) |
Walks | ||
Theorem | uhgrwkspthlem2 26650 | Lemma 2 for uhgrwkspth 26651. (Contributed by AV, 25-Jan-2021.) |
Walks | ||
Theorem | uhgrwkspth 26651 | Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
Vtx Edg WalksOn SPathsOn | ||
Theorem | usgr2wlkneq 26652 | The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
USGraph Walks | ||
Theorem | usgr2wlkspthlem1 26653 | Lemma 1 for usgr2wlkspth 26655. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
Walks USGraph | ||
Theorem | usgr2wlkspthlem2 26654 | Lemma 2 for usgr2wlkspth 26655. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) |
Walks USGraph | ||
Theorem | usgr2wlkspth 26655 | In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
USGraph WalksOn SPathsOn | ||
Theorem | usgr2trlncl 26656 | In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.) |
USGraph Trails | ||
Theorem | usgr2trlspth 26657 | In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021.) |
USGraph Trails SPaths | ||
Theorem | usgr2pthspth 26658 | In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
USGraph Paths SPaths | ||
Theorem | usgr2pthlem 26659* | Lemma for usgr2pth 26660. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
Vtx iEdg ..^ ..^ USGraph | ||
Theorem | usgr2pth 26660* | In a simple graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.) |
Vtx iEdg USGraph Paths ..^ | ||
Theorem | usgr2pth0 26661* | In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
Vtx iEdg USGraph Paths ..^ | ||
Theorem | pthdlem1 26662* | Lemma 1 for pthd 26665. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.) |
Word ..^ ..^ ..^ | ||
Theorem | pthdlem2lem 26663* | Lemma for pthdlem2 26664. (Contributed by AV, 10-Feb-2021.) |
Word ..^ ..^ ..^ | ||
Theorem | pthdlem2 26664* | Lemma 2 for pthd 26665. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.) |
Word ..^ ..^ ..^ | ||
Theorem | pthd 26665* | Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Word ..^ ..^ Trails Paths | ||
Syntax | cclwlks 26666 | Extend class notation with closed walks (of a graph). |
ClWalks | ||
Definition | df-clwlks 26667* |
Define the set of all closed walks (in an undirected graph).
According to definition 4 in [Huneke] p. 2: "A walk of length n on (a graph) G is an ordered sequence v0 , v1 , ... v(n) of vertices such that v(i) and v(i+1) are neighbors (i.e are connected by an edge). We say the walk is closed if v(n) = v0". According to the definition of a walk as two mappings f from { 0 , ... , ( n - 1 ) } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices, a closed walk is represented by the following sequence: p(0) e(f(0)) p(1) e(f(1)) ... p(n-1) e(f(n-1)) p(n)=p(0). Notice that by this definition, a single vertex is a closed walk of length 0, see also 0clwlk 26991! (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.) |
ClWalks Walks | ||
Theorem | clwlks 26668* | The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Revised by AV, 29-Oct-2021.) |
ClWalks Walks | ||
Theorem | isclwlk 26669 | A pair of functions represents a closed walk iff it represents a walk in which the first vertex is equal to the last vertex. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
ClWalks Walks | ||
Theorem | clwlkiswlk 26670 | A closed walk is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
ClWalks Walks | ||
Theorem | clwlkwlk 26671 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
ClWalks Walks | ||
Theorem | clwlkswks 26672 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Feb-2021.) |
ClWalks Walks | ||
Theorem | isclwlke 26673* | Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.) |
Vtx iEdg ClWalks Word ..^if- | ||
Theorem | isclwlkupgr 26674* | Properties of a pair of functions to be a closed walk (in a pseudograph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 11-Apr-2021.) (Revised by AV, 28-Oct-2021.) |
Vtx iEdg UPGraph ClWalks Word ..^ | ||
Theorem | clwlkcomp 26675* | A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.) |
Vtx iEdg ClWalks Word ..^if- | ||
Theorem | clwlkcompim 26676* | Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.) |
Vtx iEdg ClWalks Word ..^if- | ||
Theorem | upgrclwlkcompim 26677* | Implications for the properties of the components of a closed walk in a pseudograph. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 2-May-2021.) |
Vtx iEdg UPGraph ClWalks Word ..^ | ||
Theorem | clwlkl1loop 26678 | A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021.) |
iEdg ClWalks Edg | ||
Syntax | ccrcts 26679 | Extend class notation with circuits (in a graph). |
Circuits | ||
Syntax | ccycls 26680 | Extend class notation with cycles (in a graph). |
Cycles | ||
Definition | df-crcts 26681* |
Define the set of all circuits (in an undirected graph).
According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A circuit can be a closed walk allowing repetitions of vertices but not edges;"; according to Wikipedia ("Glossary of graph theory terms", https://en.wikipedia.org/wiki/Glossary_of_graph_theory_terms, 3-Oct-2017): "A circuit may refer to ... a trail (a closed tour without repeated edges), ...". Following Bollobas ("A trail whose endvertices coincide (a closed trail) is called a circuit.", see Definition of [Bollobas] p. 5.), a circuit is a closed trail without repeated edges. So the circuit is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
Circuits Trails | ||
Definition | df-cycls 26682* |
Define the set of all (simple) cycles (in an undirected graph).
According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A simple cycle may be defined either as a closed walk with no repetitions of vertices and edges allowed, other than the repetition of the starting and ending vertex," According to Bollobas: "If a walk W = x0 x1 ... x(l) is such that l >= 3, x0=x(l), and the vertices x(i), 0 < i < l, are distinct from each other and x0, then W is said to be a cycle.", see Definition of [Bollobas] p. 5. However, since a walk consisting of distinct vertices (except the first and the last vertex) is a path, a cycle can be defined as path whose first and last vertices coincide. So a cycle is represented by the following sequence: p(0) e(f(1)) p(1) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
Cycles Paths | ||
Theorem | crcts 26683* | The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
Circuits Trails | ||
Theorem | cycls 26684* | The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
Cycles Paths | ||
Theorem | iscrct 26685 | Sufficient and necessary conditions for a pair of functions to be a circuit (in an undirected graph): A pair of function "is" (represents) a circuit iff it is a closed trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Circuits Trails | ||
Theorem | iscycl 26686 | Sufficient and necessary conditions for a pair of functions to be a cycle (in an undirected graph): A pair of function "is" (represents) a cycle iff it is a closed path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
Cycles Paths | ||
Theorem | crctprop 26687 | The properties of a circuit: A circuit is a closed trail. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Circuits Trails | ||
Theorem | cyclprop 26688 | The properties of a cycle: A cycle is a closed path. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Cycles Paths | ||
Theorem | crctisclwlk 26689 | A circuit is a closed walk. (Contributed by AV, 17-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Circuits ClWalks | ||
Theorem | crctistrl 26690 | A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
Circuits Trails | ||
Theorem | crctiswlk 26691 | A circuit is a walk. (Contributed by AV, 6-Apr-2021.) |
Circuits Walks | ||
Theorem | cyclispth 26692 | A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
Cycles Paths | ||
Theorem | cycliswlk 26693 | A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 31-Jan-2021.) |
Cycles Walks | ||
Theorem | cycliscrct 26694 | A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Cycles Circuits | ||
Theorem | cyclnspth 26695 | A (non trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Cycles SPaths | ||
Theorem | cyclispthon 26696 | A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
Cycles PathsOn | ||
Theorem | lfgrn1cycl 26697* | In a loop-free graph there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.) |
Vtx iEdg Cycles | ||
Theorem | usgr2trlncrct 26698 | In a simple graph, any trail of length 2 is not a circuit. (Contributed by AV, 5-Jun-2021.) |
USGraph Trails Circuits | ||
Theorem | umgrn1cycl 26699 | In a multigraph graph (with no loops!) there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.) |
UMGraph Cycles | ||
Theorem | uspgrn2crct 26700 | In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 3-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.) |
USPGraph Circuits |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |