Home | Metamath
Proof Explorer Theorem List (p. 261 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cusgrares 26001* | Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) |
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ⇒ ⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑉 ∖ {𝑁}) ComplUSGrph 𝐹) | ||
Theorem | cusgrasizeindslem1 26002* | Lemma 1 for cusgrasizeinds 26004. (Contributed by Alexander van der Vekens, 11-Jan-2018.) |
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ⇒ ⊢ (dom 𝐹 ∩ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ∅ | ||
Theorem | cusgrasizeindslem2 26003* | Lemma 2 for cusgrasizeinds 26004. (Contributed by Alexander van der Vekens, 11-Jan-2018.) |
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ⇒ ⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑥)}) = ((#‘𝑉) − 1)) | ||
Theorem | cusgrasizeinds 26004* | Part 1 of induction step in cusgrasize 26006. The size of a complete simple graph with 𝑛 vertices is (𝑛 − 1) plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11-Jan-2018.) |
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ⇒ ⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘𝐸) = (((#‘𝑉) − 1) + (#‘𝐹))) | ||
Theorem | cusgrasize2inds 26005* | Induction step in cusgrasize 26006. If the size of the complete graph with 𝑛 vertices reduced by one vertex is "(𝑛 − 1) choose 2", the size of the complete graph with 𝑛 vertices is "𝑛 choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018.) |
⊢ 𝐹 = (𝐸 ↾ {𝑥 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑥)}) ⇒ ⊢ (𝑌 ∈ ℕ0 → ((𝑉 ComplUSGrph 𝐸 ∧ (#‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((#‘𝐹) = ((#‘(𝑉 ∖ {𝑁}))C2) → (#‘𝐸) = ((#‘𝑉)C2)))) | ||
Theorem | cusgrasize 26006 | The size of a finite complete simple graph with 𝑛 vertices (𝑛 ∈ ℕ0) is (𝑛C2) ("𝑛 choose 2") resp. (((𝑛 − 1)∗𝑛) / 2). (Contributed by Alexander van der Vekens, 11-Jan-2018.) |
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑉 ∈ Fin) → (#‘𝐸) = ((#‘𝑉)C2)) | ||
Theorem | cusgrafilem1 26007* | Lemma 1 for cusgrafi 26010. (Contributed by Alexander van der Vekens, 13-Jan-2018.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} ⇒ ⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → 𝑃 ⊆ ran 𝐸) | ||
Theorem | cusgrafilem2 26008* | Lemma 2 for cusgrafi 26010. (Contributed by Alexander van der Vekens, 13-Jan-2018.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃) | ||
Theorem | cusgrafilem3 26009* | Lemma 3 for cusgrafi 26010. (Contributed by Alexander van der Vekens, 13-Jan-2018.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → (¬ 𝑉 ∈ Fin → ¬ 𝑃 ∈ Fin)) | ||
Theorem | cusgrafi 26010 | If the size of a complete simple graph is finite, then also its order is finite. (Contributed by Alexander van der Vekens, 13-Jan-2018.) |
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝐸 ∈ Fin) → 𝑉 ∈ Fin) | ||
Theorem | usgrasscusgra 26011* | An undirected simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ∀𝑒 ∈ ran 𝐸∃𝑓 ∈ ran 𝐹 𝑒 = 𝑓) | ||
Theorem | sizeusglecusglem1 26012 | Lemma 1 for sizeusglecusg 26014. (Contributed by Alexander van der Vekens, 12-Jan-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → ( I ↾ ran 𝐸):ran 𝐸–1-1→ran 𝐹) | ||
Theorem | sizeusglecusglem2 26013 | Lemma 2 for sizeusglecusg 26014. (Contributed by Alexander van der Vekens, 13-Jan-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹 ∧ 𝐹 ∈ Fin) → 𝐸 ∈ Fin) | ||
Theorem | sizeusglecusg 26014 | The size of an undirected simple graph with 𝑛 vertices is at most the size of a complete simple graph with 𝑛 vertices (𝑛 may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Proof shortened by AV, 4-May-2021.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ComplUSGrph 𝐹) → (#‘𝐸) ≤ (#‘𝐹)) | ||
Theorem | usgramaxsize 26015 | The maximum size of an undirected simple graph with 𝑛 vertices (𝑛 ∈ ℕ0) is (((𝑛 − 1)∗𝑛) / 2). (Contributed by Alexander van der Vekens, 13-Jan-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (#‘𝐸) ≤ ((#‘𝑉)C2)) | ||
Theorem | isuvtx 26016* | The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 UnivVertex 𝐸) = {𝑛 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑛}){𝑘, 𝑛} ∈ ran 𝐸}) | ||
Theorem | uvtxel 26017* | A universal vertex, i.e. an element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁}){𝑘, 𝑁} ∈ ran 𝐸))) | ||
Theorem | uvtxisvtx 26018 | A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
⊢ (𝑁 ∈ (𝑉 UnivVertex 𝐸) → 𝑁 ∈ 𝑉) | ||
Theorem | uvtx0 26019 | There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
⊢ (∅ UnivVertex 𝐸) = ∅ | ||
Theorem | uvtx01vtx 26020* | If a graph/class has no edges, it has universal vertices if and only if it has exactly one vertex. This theorem could have been stated ((𝑉 UnivVertex ∅) ≠ ∅ ↔ (#‘𝑉) = 1), but a lot of auxiliary theorems would have been needed. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
⊢ ((𝑉 UnivVertex ∅) ≠ ∅ ↔ ∃𝑥 𝑉 = {𝑥}) | ||
Theorem | uvtxnbgra 26021 | A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (𝑉 UnivVertex 𝐸)) → (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁})) | ||
Theorem | uvtxnm1nbgra 26022 | A universal vertex has 𝑛 − 1 neighbors in a graph with 𝑛 vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑁)) = ((#‘𝑉) − 1))) | ||
Theorem | uvtxnbgravtx 26023* | A universal vertex is neighbor of all other vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (𝑉 UnivVertex 𝐸)) → ∀𝑣 ∈ (𝑉 ∖ {𝑁})𝑁 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑣)) | ||
Theorem | cusgrauvtxb 26024 | An undirected simple graph is complete if and only if each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by Alexander van der Vekens, 18-Jan-2018.) |
⊢ (𝑉 USGrph 𝐸 → (𝑉 ComplUSGrph 𝐸 ↔ (𝑉 UnivVertex 𝐸) = 𝑉)) | ||
Theorem | uvtxnb 26025 | A vertex in a undirected simple graph is universal iff all the other vertices are its neighbors. (Contributed by Alexander van der Vekens, 13-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ 𝑉) → (𝑁 ∈ (𝑉 UnivVertex 𝐸) ↔ (〈𝑉, 𝐸〉 Neighbors 𝑁) = (𝑉 ∖ {𝑁}))) | ||
Syntax | cwalk 26026 | Extend class notation with Walks (of a graph). |
class Walks | ||
Syntax | ctrail 26027 | Extend class notation with Trails (of a graph). |
class Trails | ||
Syntax | cpath 26028 | Extend class notation with Paths (of a graph). |
class Paths | ||
Syntax | cspath 26029 | Extend class notation with Simple Paths (of a graph). |
class SPaths | ||
Syntax | cwlkon 26030 | Extend class notation with Walks between two vertices (within a graph). |
class WalkOn | ||
Syntax | ctrlon 26031 | Extend class notation with Trails between two vertices (within a graph). |
class TrailOn | ||
Syntax | cpthon 26032 | Extend class notation with Paths between two vertices (within a graph). |
class PathOn | ||
Syntax | cspthon 26033 | Extend class notation with simple paths between two vertices (within a graph). |
class SPathOn | ||
Syntax | ccrct 26034 | Extend class notation with Circuits (of a graph). |
class Circuits | ||
Syntax | ccycl 26035 | Extend class notation with Cycles (of a graph). |
class Cycles | ||
Definition | df-wlk 26036* |
Define the set of all Walks (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A walk of length k in a graph is an alternating sequence of vertices and edges, v0 , e0 , v1 , e1 , v2 , ... , v(k-1) , e(k-1) , v(k) which begins and ends with vertices. If the graph is undirected, then the endpoints of e(i) are v(i) and v(i+1)." According to Bollobas: " A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. Therefore, a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is 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.) |
⊢ Walks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝑒 ∧ 𝑝:(0...(#‘𝑓))⟶𝑣 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝑒‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | ||
Definition | df-trail 26037* |
Define the set of all Trails (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A trail is a walk in which all edges are distinct. According to Bollobas: "... walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5. Therefore, a trail can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the trail 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.) |
⊢ Trails = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ Fun ◡𝑓)}) | ||
Definition | df-pth 26038* |
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 wlkdvspth 26138). 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.) |
⊢ Paths = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Trails 𝑒)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)}) | ||
Definition | df-spth 26039* |
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.) |
⊢ SPaths = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Trails 𝑒)𝑝 ∧ Fun ◡𝑝)}) | ||
Definition | df-crct 26040* |
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.) |
⊢ Circuits = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Trails 𝑒)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Definition | df-cycl 26041* |
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.) |
⊢ Cycles = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Paths 𝑒)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Definition | df-wlkon 26042* | Define the collection of walks with particular endpoints (in an un- directed graph). This corresponds to the "x0-x(l)-walks", see Definition in [Bollobas] p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) |
⊢ WalkOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) | ||
Definition | df-trlon 26043* | Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) |
⊢ TrailOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Trails 𝑒)𝑝)})) | ||
Definition | df-pthon 26044* | Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) |
⊢ PathOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 Paths 𝑒)𝑝)})) | ||
Definition | df-spthon 26045* | Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
⊢ SPathOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ 𝑓(𝑣 SPaths 𝑒)𝑝)})) | ||
Theorem | relwlk 26046 | The walks (in an undirected simple graph) are (ordered) pairs. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
⊢ Rel (𝑉 Walks 𝐸) | ||
Theorem | wlks 26047* | The set of walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 Walks 𝐸) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐸 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | ||
Theorem | iswlk 26048* | Properties of a pair of functions to be a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | 2mwlk 26049 | The two mappings determining a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) |
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) | ||
Theorem | wlkres 26050* | Restrictions of walks (i.e. special kinds of walks, for example paths - see pths 26096) are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
⊢ (𝑓(𝑉𝑊𝐸)𝑝 → 𝑓(𝑉 Walks 𝐸)𝑝) ⇒ ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉𝑊𝐸)𝑝 ∧ 𝜑)} ∈ V) | ||
Theorem | wlkbprop 26051 | Basic properties of a walk. (Contributed by Alexander van der Vekens, 31-Oct-2017.) |
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | ||
Theorem | iswlkg 26052* | Generalisation of iswlk 26048: Properties of a pair of functions to be a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹(𝑉 Walks 𝐸)𝑃 ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | wlkcomp 26053* | A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (𝑉 Walks 𝐸) ↔ (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | wlkcompim 26054* | Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) | ||
Theorem | wlkn0 26055 | The set of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018.) |
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → 𝑃 ≠ ∅) | ||
Theorem | wlkop 26056 | A walk (in an undirected simple graph) is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → 𝑊 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) | ||
Theorem | wlkcpr 26057 | A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) ↔ (1st ‘𝑊)(𝑉 Walks 𝐸)(2nd ‘𝑊)) | ||
Theorem | wlkelwrd 26058 | The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
⊢ (𝑊 ∈ (𝑉 Walks 𝐸) → ((1st ‘𝑊) ∈ Word dom 𝐸 ∧ (2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶𝑉)) | ||
Theorem | edgwlk 26059* | The (connected) edges of a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ ran 𝐸) | ||
Theorem | wlklenvm1 26060 | The number of edges of a walk (in an undirected graph) is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (#‘𝐹) = ((#‘𝑃) − 1)) | ||
Theorem | wlkon 26061* | The set of walks between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 12-Dec-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 WalkOn 𝐸)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)}) | ||
Theorem | iswlkon 26062 | Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) | ||
Theorem | wlkonprop 26063 | Properties of a walk between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) |
⊢ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) | ||
Theorem | wlkoniswlk 26064 | A walk between to vertices is a walk. (Contributed by Alexander van der Vekens, 12-Dec-2017.) |
⊢ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) | ||
Theorem | wlkonwlk 26065 | A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017.) |
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → 𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘(#‘𝐹)))𝑃) | ||
Theorem | trls 26066* | The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 Trails 𝐸) = {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐸 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | ||
Theorem | istrl 26067* | Properties of a pair of functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | istrl2 26068* | Properties of a pair of functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | trliswlk 26069 | A trail is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) |
⊢ (𝐹(𝑉 Trails 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) | ||
Theorem | trlon 26070* | The set of trails between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 4-Nov-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 TrailOn 𝐸)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ 𝑓(𝑉 Trails 𝐸)𝑝)}) | ||
Theorem | istrlon 26071 | Properties of a pair of functions to be a trail between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐹(𝐴(𝑉 TrailOn 𝐸)𝐵)𝑃 ↔ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 Trails 𝐸)𝑃))) | ||
Theorem | trlonprop 26072 | Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) |
⊢ (𝐹(𝐴(𝑉 TrailOn 𝐸)𝐵)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) ∧ (𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃 ∧ 𝐹(𝑉 Trails 𝐸)𝑃))) | ||
Theorem | trlonistrl 26073 | A trail between to vertices is a trail. (Contributed by Alexander van der Vekens, 12-Dec-2017.) |
⊢ (𝐹(𝐴(𝑉 TrailOn 𝐸)𝐵)𝑃 → 𝐹(𝑉 Trails 𝐸)𝑃) | ||
Theorem | trlonwlkon 26074 | A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
⊢ (𝐹(𝐴(𝑉 TrailOn 𝐸)𝐵)𝑃 → 𝐹(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑃) | ||
Theorem | 0wlk 26075 | A pair of an empty set (of edges) and a second set (of vertices) is a walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑃 ∈ 𝑍) → (∅(𝑉 Walks 𝐸)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0trl 26076 | A pair of an empty set (of edges) and a second set (of vertices) is a trail if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Proof shortened by AV, 7-Jan-2020.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑃 ∈ 𝑍) → (∅(𝑉 Trails 𝐸)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0wlkon 26077 | A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑁 ∈ 𝑉) → ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(𝑉 WalkOn 𝐸)𝑁)𝑃)) | ||
Theorem | 0trlon 26078 | A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑁 ∈ 𝑉) → ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(𝑉 TrailOn 𝐸)𝑁)𝑃)) | ||
Theorem | 2trllemF 26079 | Lemma 5 for constr2trl 26129. (Contributed by Alexander van der Vekens, 31-Jan-2018.) |
⊢ (((𝐸‘𝐼) = {𝑋, 𝑌} ∧ 𝑌 ∈ 𝑉) → 𝐼 ∈ dom 𝐸) | ||
Theorem | 2trllemA 26080 | Lemma 1 for constr2trl 26129. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by Alexander van der Vekens, 31-Jan-2018.) |
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) & ⊢ 𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} ⇒ ⊢ (#‘𝐹) = 2 | ||
Theorem | 2trllemB 26081 | Lemma 2 for constr2trl 26129. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by Alexander van der Vekens, 31-Jan-2018.) |
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) & ⊢ 𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} ⇒ ⊢ (0..^(#‘𝐹)) = {0, 1} | ||
Theorem | 2trllemH 26082 | Lemma 3 for constr2trl 26129. (Contributed by Alexander van der Vekens, 31-Jan-2018.) |
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) & ⊢ 𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} ⇒ ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) | ||
Theorem | 2trllemE 26083 | Lemma 4 for constr2trl 26129. (Contributed by Alexander van der Vekens, 31-Jan-2018.) |
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) & ⊢ 𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} ⇒ ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) | ||
Theorem | 2wlklemA 26084 | Lemma for constr2wlk 26128. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑃‘0) = 𝐴) | ||
Theorem | 2wlklemB 26085 | Lemma for constr2wlk 26128. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → (𝑃‘1) = 𝐵) | ||
Theorem | 2wlklemC 26086 | Lemma for constr2wlk 26128. (Contributed by Alexander van der Vekens, 18-Feb-2018.) |
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ⇒ ⊢ (𝐶 ∈ 𝑉 → (𝑃‘2) = 𝐶) | ||
Theorem | 2trllemD 26087 | Lemma 4 for constr2trl 26129. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by Alexander van der Vekens, 31-Jan-2018.) |
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃 Fn {0, 1, 2}) | ||
Theorem | 2trllemG 26088 | Lemma 7 for constr2trl 26129. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃:(0...2)⟶𝑉) | ||
Theorem | wlkntrllem1 26089 | Lemma 1 for wlkntrl 26092: F is a word over {0}, the domain of E. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) |
⊢ 𝑉 = {𝑥, 𝑦} & ⊢ 𝐸 = {〈0, {𝑥, 𝑦}〉} & ⊢ 𝐹 = {〈0, 0〉, 〈1, 0〉} & ⊢ 𝑃 = {〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉} ⇒ ⊢ 𝐹 ∈ Word dom 𝐸 | ||
Theorem | wlkntrllem2 26090* | Lemma 2 for wlkntrl 26092: The values of E after F are edges between two vertices enumerated by P. (Contributed by Alexander van der Vekens, 22-Oct-2017.) |
⊢ 𝑉 = {𝑥, 𝑦} & ⊢ 𝐸 = {〈0, {𝑥, 𝑦}〉} & ⊢ 𝐹 = {〈0, 0〉, 〈1, 0〉} & ⊢ 𝑃 = {〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉} ⇒ ⊢ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} | ||
Theorem | wlkntrllem3 26091* | Lemma 3 for wlkntrl 26092: F is not injective. (Contributed by Alexander van der Vekens, 22-Oct-2017.) |
⊢ 𝑉 = {𝑥, 𝑦} & ⊢ 𝐸 = {〈0, {𝑥, 𝑦}〉} & ⊢ 𝐹 = {〈0, 0〉, 〈1, 0〉} & ⊢ 𝑃 = {〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉} ⇒ ⊢ ¬ Fun ◡𝐹 | ||
Theorem | wlkntrl 26092* | A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one edge to the other is a walk, but not a trail. Notice that 〈𝑉, 𝐸〉 is a simple graph (without loops) only if 𝑥 ≠ 𝑦. (Contributed by Alexander van der Vekens, 22-Oct-2017.) |
⊢ 𝑉 = {𝑥, 𝑦} & ⊢ 𝐸 = {〈0, {𝑥, 𝑦}〉} & ⊢ 𝐹 = {〈0, 0〉, 〈1, 0〉} & ⊢ 𝑃 = {〈0, 𝑥〉, 〈1, 𝑦〉, 〈2, 𝑥〉} ⇒ ⊢ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ ¬ 𝐹(𝑉 Trails 𝐸)𝑃) | ||
Theorem | usgrwlknloop 26093* | In an undirected simple graph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Walks 𝐸)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | 2wlklem 26094* | Lemma for is2wlk 26095 and 2wlklemA 26084. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
⊢ (∀𝑘 ∈ {0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) | ||
Theorem | is2wlk 26095 | Properties of a pair of functions to be a walk of length 2 (in an undirected graph). (Contributed by Alexander van der Vekens, 16-Feb-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 2) ↔ (𝐹:(0..^2)⟶dom 𝐸 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) | ||
Theorem | pths 26096* | The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 Paths 𝐸) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)}) | ||
Theorem | spths 26097* | The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 SPaths 𝐸) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Trails 𝐸)𝑝 ∧ Fun ◡𝑝)}) | ||
Theorem | ispth 26098 | Properties of a pair of functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 Paths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) | ||
Theorem | isspth 26099 | Properties of a pair of functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 SPaths 𝐸)𝑃 ↔ (𝐹(𝑉 Trails 𝐸)𝑃 ∧ Fun ◡𝑃))) | ||
Theorem | 0pth 26100 | A pair of an empty set (of edges) and a second set (of vertices) is a path if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑃 ∈ 𝑍) → (∅(𝑉 Paths 𝐸)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |