Home | Metamath
Proof Explorer Theorem List (p. 410 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 | ||
Definition | df-trls 40901* |
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.) (Revised by AV, 28-Dec-2020.) |
⊢ TrailS = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(1Walks‘𝑔)𝑝 ∧ Fun ◡𝑓)}) | ||
Definition | df-trlson 40902* | Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
⊢ TrailsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(WalksOn‘𝑔)𝑏)𝑝 ∧ 𝑓(TrailS‘𝑔)𝑝)})) | ||
Theorem | trlsfval 40903* | The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Proof shortened by AV, 31-Jan-2021.) |
⊢ (𝐺 ∈ 𝑊 → (TrailS‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(1Walks‘𝐺)𝑝 ∧ Fun ◡𝑓)}) | ||
Theorem | isTrl 40904 | Conditions for a pair of functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Proof shortened by AV, 31-Jan-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(TrailS‘𝐺)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝐹))) | ||
Theorem | trlis1wlk 40905 | A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) |
⊢ (𝐹(TrailS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | trlf1 40906 | The enumeration 𝐹 of a trail 〈𝐹, 𝑃〉 is injective. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(TrailS‘𝐺)𝑃 → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼) | ||
Theorem | trlreslem 40907 | Lemma for trlres 40908. Formerly part of proof of eupthres 41383. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(TrailS‘𝐺)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹))) & ⊢ 𝐻 = (𝐹 ↾ (0..^𝑁)) ⇒ ⊢ (𝜑 → 𝐻:(0..^(#‘𝐻))–1-1-onto→dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))) | ||
Theorem | trlres 40908 | The restriction 〈𝐻, 𝑄〉 of a trail 〈𝐹, 𝑃〉 to an initial segment of the trail (of length 𝑁) forms a trail on the subgraph 𝑆 consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(TrailS‘𝐺)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹))) & ⊢ 𝐻 = (𝐹 ↾ (0..^𝑁)) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) ⇒ ⊢ (𝜑 → 𝐻(TrailS‘𝑆)𝑄) | ||
Theorem | upgrtrls 40909* | The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → (TrailS‘𝐺) = {〈𝑓, 𝑝〉 ∣ ((𝑓 ∈ Word dom 𝐼 ∧ Fun ◡𝑓) ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | ||
Theorem | upgristrl 40910* | Properties of a pair of functions to be a trail in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(TrailS‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ Fun ◡𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | upgrf1istrl 40911* | Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(TrailS‘𝐺)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | 1wlksonproplem 40912* | Lemma for theorems for properties of walks between two vertices, e.g. trlsonprop 40915. (Contributed by AV, 16-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃))) & ⊢ 𝑊 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(𝑂‘𝑔)𝑏)𝑝 ∧ 𝑓(𝑄‘𝑔)𝑝)})) & ⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝑓(𝑄‘𝐺)𝑝) → 𝑓(1Walks‘𝐺)𝑝) ⇒ ⊢ (𝐹(𝐴(𝑊‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(𝑂‘𝐺)𝐵)𝑃 ∧ 𝐹(𝑄‘𝐺)𝑃))) | ||
Theorem | trlsonfval 40913* | 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 40914 | 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 40915 | 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‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐹(TrailS‘𝐺)𝑃))) | ||
Theorem | trlsonistrl 40916 | 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 40917 | 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 40918 | A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝐹(TrailS‘𝐺)𝑃 → 𝐹((𝑃‘0)(TrailsOn‘𝐺)(𝑃‘(#‘𝐹)))𝑃) | ||
Syntax | cpths 40919 | Extend class notation with paths (of a graph). |
class PathS | ||
Syntax | cspths 40920 | Extend class notation with simple paths (of a graph). |
class SPathS | ||
Syntax | cpthson 40921 | Extend class notation with paths between two vertices (within a graph). |
class PathsOn | ||
Syntax | cspthson 40922 | Extend class notation with simple paths between two vertices (within a graph). |
class SPathsOn | ||
Definition | df-pths 40923* |
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.) (Revised by AV, 9-Jan-2021.) |
⊢ PathS = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(TrailS‘𝑔)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)}) | ||
Definition | df-spths 40924* |
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 = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(TrailS‘𝑔)𝑝 ∧ Fun ◡𝑝)}) | ||
Definition | df-pthson 40925* | 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 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(PathS‘𝑔)𝑝)})) | ||
Definition | df-spthson 40926* | 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 = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(SPathS‘𝑔)𝑝)})) | ||
Theorem | pthsfval 40927* | The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.) |
⊢ (𝐺 ∈ 𝑊 → (PathS‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(TrailS‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(#‘𝑓))) ∧ ((𝑝 “ {0, (#‘𝑓)}) ∩ (𝑝 “ (1..^(#‘𝑓)))) = ∅)}) | ||
Theorem | spthsfval 40928* | The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.) |
⊢ (𝐺 ∈ 𝑊 → (SPathS‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(TrailS‘𝐺)𝑝 ∧ Fun ◡𝑝)}) | ||
Theorem | isPth 40929 | Conditions for a pair of functions to be 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, 31-Jan-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(PathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) ∧ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅))) | ||
Theorem | issPth 40930 | Conditions for a pair of 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.) (Proof shortened by AV, 31-Jan-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(SPathS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ Fun ◡𝑃))) | ||
Theorem | PthisTrl 40931 | A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ (𝐹(PathS‘𝐺)𝑃 → 𝐹(TrailS‘𝐺)𝑃) | ||
Theorem | sPthisPth 40932 | 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.) |
⊢ (𝐹(SPathS‘𝐺)𝑃 → 𝐹(PathS‘𝐺)𝑃) | ||
Theorem | pthis1wlk 40933 | A path is a 1-walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.) |
⊢ (𝐹(PathS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | sPthis1wlk 40934 | A simple path is a 1-walk (in an undirected graph). (Contributed by AV, 16-May-2021.) |
⊢ (𝐹(SPathS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | pthdivtx 40935 | The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.) |
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝐼 ∈ (1..^(#‘𝐹)) ∧ 𝐽 ∈ (0...(#‘𝐹)) ∧ 𝐼 ≠ 𝐽)) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)) | ||
Theorem | pthdadjvtx 40936 | The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.) |
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 𝐼 ∈ (0..^(#‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘(𝐼 + 1))) | ||
Theorem | 2pthnloop 40937* | 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 41318. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹)) → ∀𝑖 ∈ (0..^(#‘𝐹))2 ≤ (#‘(𝐼‘(𝐹‘𝑖)))) | ||
Theorem | upgr2pthnlp 40938* | A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹)) → ∀𝑖 ∈ (0..^(#‘𝐹))(#‘(𝐼‘(𝐹‘𝑖))) = 2) | ||
Theorem | sPthdifv 40939 | 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.) |
⊢ (𝐹(SPathS‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))–1-1→(Vtx‘𝐺)) | ||
Theorem | spthdep 40940 | A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.) |
⊢ ((𝐹(SPathS‘𝐺)𝑃 ∧ (#‘𝐹) ≠ 0) → (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) | ||
Theorem | pthdepissPth 40941 | 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.) |
⊢ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹))) → 𝐹(SPathS‘𝐺)𝑃) | ||
Theorem | upgrwlkdvdelem 40942* | Lemma for upgrwlkdvde 40943. Formerly wlkdvspthlem 26137. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.) |
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ 𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹)) | ||
Theorem | upgrwlkdvde 40943 | 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 upgrspths1wlk 40944. (Contributed by AV, 17-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → Fun ◡𝐹) | ||
Theorem | upgrspths1wlk 40944* | 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.) |
⊢ (𝐺 ∈ UPGraph → (SPathS‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(1Walks‘𝐺)𝑝 ∧ Fun ◡𝑝)}) | ||
Theorem | upgrwlkdvspth 40945 | A walk consisting of different vertices is a simple path. Formerly wlkdvspth 26138. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspths1wlk 40944. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → 𝐹(SPathS‘𝐺)𝑃) | ||
Theorem | pthsonfval 40946* | 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 40947* | 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 40948 | 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 40949 | 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 40950 | Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(PathS‘𝐺)𝑃))) | ||
Theorem | spthonprop 40951 | 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‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPathS‘𝐺)𝑃))) | ||
Theorem | pthonispth-av 40952 | 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 40953 | A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.) |
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃) | ||
Theorem | pthOnpth 40954 | A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝐹(PathS‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘(#‘𝐹)))𝑃) | ||
Theorem | isspthonpth-av 40955 | 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‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) | ||
Theorem | spthonisspth-av 40956 | 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 40957 | A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.) |
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃) | ||
Theorem | spthonepeq-av 40958 | 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.) |
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (#‘𝐹) = 0)) | ||
Theorem | uhgr1wlkspthlem1 40959 | Lemma 1 for uhgr1wlkspth 40961. (Contributed by AV, 25-Jan-2021.) |
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (#‘𝐹) = 1) → Fun ◡𝐹) | ||
Theorem | uhgr1wlkspthlem2 40960 | Lemma 2 for uhgr1wlkspth 40961. (Contributed by AV, 25-Jan-2021.) |
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ ((#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → Fun ◡𝑃) | ||
Theorem | uhgr1wlkspth 40961 | Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ (#‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) | ||
Theorem | usgr2wlkneq 40962 | 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 ∧ 𝐹(1Walks‘𝐺)𝑃) ∧ ((#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) | ||
Theorem | usgr2wlkspthlem1 40963 | Lemma 1 for usgr2wlkspth 40965. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) → Fun ◡𝐹) | ||
Theorem | usgr2wlkspthlem2 40964 | Lemma 2 for usgr2wlkspth 40965. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) |
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (#‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) → Fun ◡𝑃) | ||
Theorem | usgr2wlkspth 40965 | 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.) |
⊢ ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) | ||
Theorem | usgr2trlncl 40966 | In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝐹(TrailS‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2))) | ||
Theorem | usgr2trlspth 40967 | In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝐹(TrailS‘𝐺)𝑃 ↔ 𝐹(SPathS‘𝐺)𝑃)) | ||
Theorem | usgr2pthspth 40968 | 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 ∧ (#‘𝐹) = 2) → (𝐹(PathS‘𝐺)𝑃 ↔ 𝐹(SPathS‘𝐺)𝑃)) | ||
Theorem | usgr2pthlem 40969* | Lemma for usgr2pth 40970. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))) | ||
Theorem | usgr2pth 40970* | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → ((𝐹(PathS‘𝐺)𝑃 ∧ (#‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) | ||
Theorem | usgr2pth0 40971* | 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‘𝐺)𝑃 ∧ (#‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑧 ∧ (𝑃‘2) = 𝑦) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑧} ∧ (𝐼‘(𝐹‘1)) = {𝑧, 𝑦}))))) | ||
Theorem | pthdlem1 40972* | Lemma 1 for pthd 40975. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((#‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(#‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ (𝜑 → Fun ◡(𝑃 ↾ (1..^𝑅))) | ||
Theorem | pthdlem2lem 40973* | Lemma for pthdlem2 40974. (Contributed by AV, 10-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((#‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(#‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ ((𝜑 ∧ (#‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅))) | ||
Theorem | pthdlem2 40974* | Lemma 2 for pthd 40975. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((#‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(#‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) | ||
Theorem | pthd 40975* | Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((#‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(#‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) & ⊢ (#‘𝐹) = 𝑅 & ⊢ (𝜑 → 𝐹(TrailS‘𝐺)𝑃) ⇒ ⊢ (𝜑 → 𝐹(PathS‘𝐺)𝑃) | ||
Syntax | cclwlks 40976 | Extend class notation with closed walks (of a graph). |
class ClWalkS | ||
Definition | df-clwlks 40977* |
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 41298! (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.) |
⊢ ClWalkS = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(1Walks‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Theorem | clwlkS 40978* | The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) |
⊢ (𝐺 ∈ 𝑋 → (ClWalkS‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(1Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Theorem | isclWlk 40979 | Properties of a pair of functions to be a closed walk (in an undirected graph) in terms of walks. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) |
⊢ ((𝐺 ∈ 𝑋 ∧ 𝐹 ∈ 𝑌 ∧ 𝑃 ∈ 𝑍) → (𝐹(ClWalkS‘𝐺)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | isclWlkb 40980 | Generalisation of isclwlk 26284: 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.) |
⊢ (𝐹(ClWalkS‘𝐺)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) | ||
Theorem | clwlkis1wlk 40981 | 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.) |
⊢ (𝐹(ClWalkS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | clwlk1wlk 40982 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 16-Feb-2021.) |
⊢ (𝑊 ∈ (ClWalkS‘𝐺) → 𝑊 ∈ (1Walks‘𝐺)) | ||
Theorem | clwlks1wlks 40983 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Feb-2021.) |
⊢ (ClWalkS‘𝐺) ⊆ (1Walks‘𝐺) | ||
Theorem | isclWlke 40984* | 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 dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))) | ||
Theorem | isclWlkupgr 40985* | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(ClWalkS‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))) | ||
Theorem | clWlkcomp 40986* | 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‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝐺 ∈ 𝑋 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (ClWalkS‘𝐺) ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))) | ||
Theorem | clWlkcompim 40987* | 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‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (ClWalkS‘𝐺) → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | upgrclwlkcompim 40988* | 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‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (ClWalkS‘𝐺)) → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) | ||
Theorem | clwlkl1loop 40989 | A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021.) |
⊢ ((Fun (iEdg‘𝐺) ∧ 𝐹(ClWalkS‘𝐺)𝑃 ∧ (#‘𝐹) = 1) → ((𝑃‘0) = (𝑃‘1) ∧ {(𝑃‘0)} ∈ (Edg‘𝐺))) | ||
Syntax | ccrcts 40990 | Extend class notation with circuits (in a graph). |
class CircuitS | ||
Syntax | ccycls 40991 | Extend class notation with cycles (in a graph). |
class CycleS | ||
Definition | df-crcts 40992* |
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 = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(TrailS‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Definition | df-cycls 40993* |
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 = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(PathS‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Theorem | crctS 40994* | 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‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Theorem | cyclS 40995* | 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‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Theorem | isCrct 40996 | 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.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(CircuitS‘𝐺)𝑃 ↔ (𝐹(TrailS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | isCycl 40997 | 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.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(CycleS‘𝐺)𝑃 ↔ (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | crctprop 40998 | The properties of a circuit: A circuit is a closed trail. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝐹(CircuitS‘𝐺)𝑃 → (𝐹(TrailS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) | ||
Theorem | cyclprop 40999 | The properties of a cycle: A cycle is a closed path. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝐹(CycleS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) | ||
Theorem | crctisclwlk 41000 | A circuit is a closed walk. (Contributed by AV, 17-Feb-2021.) |
⊢ (𝐹(CircuitS‘𝐺)𝑃 → 𝐹(ClWalkS‘𝐺)𝑃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |