Home | Metamath
Proof Explorer Theorem List (p. 263 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 | isconngra1 26201* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ConnGrph 𝐸 ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(𝑉 PathOn 𝐸)𝑛)𝑝)) | ||
Theorem | 0conngra 26202 | A class/graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) |
⊢ (𝐸 ∈ 𝑉 → ∅ ConnGrph 𝐸) | ||
Theorem | 1conngra 26203 | A class/graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) |
⊢ (𝐸 ∈ 𝑉 → {𝐴} ConnGrph 𝐸) | ||
Theorem | cusconngra 26204 | A complete (undirected simple) graph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.) |
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 ConnGrph 𝐸) | ||
Syntax | cwwlk 26205 | Extend class notation with Walks (of a graph) as Word over the set of vertices. |
class WWalks | ||
Syntax | cwwlkn 26206 | Extend class notation with Walks (of a graph) of a fixed length as Word over the set of vertices. |
class WWalksN | ||
Definition | df-wwlk 26207* | Define the set of all Walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlk 26036. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 26055. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ WWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)}) | ||
Definition | df-wwlkn 26208* | Define the set of all Walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlk 26036. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ WWalksN = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 WWalks 𝑒) ∣ (#‘𝑤) = (𝑛 + 1)})) | ||
Theorem | wwlk 26209* | The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 WWalks 𝐸) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸)}) | ||
Theorem | wwlkn 26210* | The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑉 WWalksN 𝐸)‘𝑁) = {𝑤 ∈ (𝑉 WWalks 𝐸) ∣ (#‘𝑤) = (𝑁 + 1)}) | ||
Theorem | iswwlk 26211* | Properties of a word to represent a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑊 ∈ (𝑉 WWalks 𝐸) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸))) | ||
Theorem | iswwlkn 26212 | Properties of a word to represent a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ↔ (𝑊 ∈ (𝑉 WWalks 𝐸) ∧ (#‘𝑊) = (𝑁 + 1)))) | ||
Theorem | wwlkprop 26213 | Properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ (𝑃 ∈ (𝑉 WWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)) | ||
Theorem | wwlknprop 26214 | Properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018.) |
⊢ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑃 ∈ Word 𝑉))) | ||
Theorem | wwlknimp 26215* | Implications for a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) |
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸)) | ||
Theorem | wwlksswrd 26216 | Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) |
⊢ (𝑉 WWalks 𝐸) ⊆ Word 𝑉 | ||
Theorem | wwlkn0 26217* | A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘0) → ∃𝑣 ∈ 𝑉 𝑊 = 〈“𝑣”〉) | ||
Theorem | wlkiswwlk1 26218 | The sequence of vertices in a walk is a walk as word in an undirected simple graph. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ (𝑉 USGrph 𝐸 → (𝐹(𝑉 Walks 𝐸)𝑃 → 𝑃 ∈ (𝑉 WWalks 𝐸))) | ||
Theorem | wlkiswwlk2lem1 26219* | Lemma 1 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) | ||
Theorem | wlkiswwlk2lem2 26220* | Lemma 2 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ (((#‘𝑃) ∈ ℕ0 ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) | ||
Theorem | wlkiswwlk2lem3 26221* | Lemma 3 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → 𝑃:(0...(#‘𝐹))⟶𝑉) | ||
Theorem | wlkiswwlk2lem4 26222* | Lemma 4 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | ||
Theorem | wlkiswwlk2lem5 26223* | Lemma 5 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸)) | ||
Theorem | wlkiswwlk2lem6 26224* | Lemma 6 for wlkiswwlk2 26225. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) | ||
Theorem | wlkiswwlk2 26225* | A walk as word corresponds to the sequence of vertices in a walk in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 WWalks 𝐸) → ∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃)) | ||
Theorem | wlkiswwlk 26226* | A walk as word corresponds to a walk in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ (𝑉 USGrph 𝐸 → (∃𝑓 𝑓(𝑉 Walks 𝐸)𝑃 ↔ 𝑃 ∈ (𝑉 WWalks 𝐸))) | ||
Theorem | wlklniswwlkn1 26227 | The sequence of vertices in a walk of length n is a walk as word of length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ (𝑉 USGrph 𝐸 → ((𝐹(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝐹) = 𝑁) → 𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) | ||
Theorem | wlklniswwlkn2 26228* | A walk of length n as word corresponds to the sequence of vertices in a walk of length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁))) | ||
Theorem | wlklniswwlkn 26229* | A walk of length n as word corresponds to a walk with length n in an undirected simple graph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) |
⊢ (𝑉 USGrph 𝐸 → (∃𝑓(𝑓(𝑉 Walks 𝐸)𝑃 ∧ (#‘𝑓) = 𝑁) ↔ 𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) | ||
Theorem | wwlkiswwlkn 26230 | A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018.) |
⊢ (𝑃 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝑃 ∈ (𝑉 WWalks 𝐸)) | ||
Theorem | wwlksswwlkn 26231 | The walks of a fixed length as words are walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) |
⊢ ((𝑉 WWalksN 𝐸)‘𝑁) ⊆ (𝑉 WWalks 𝐸) | ||
Theorem | wwlknimpb 26232 | Basic implications for a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 3-Oct-2018.) |
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1))) | ||
Theorem | wwlkn0s 26233* | The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → ((𝑉 WWalksN 𝐸)‘0) = {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 1}) | ||
Theorem | vfwlkniswwlkn 26234 | If the edge function of a walk has length n, then the vertex function of the walk is a word representing the walk as word of length n. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊) ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) | ||
Theorem | 2wlkeq 26235* | Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.) |
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) | ||
Theorem | usg2wlkeq 26236* | Conditions for two walks within the same undirected simple graph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ (𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸)) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)))) | ||
Theorem | usg2wlkeq2 26237 | Conditions for which two walks within the same undirected simple graph are the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st ‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st ‘𝑊)) = 𝑁)) → ((2nd ‘𝑋) = (2nd ‘𝑊) → 𝑋 = 𝑊)) | ||
Theorem | wlknwwlknfun 26238* | Lemma 1 for wlknwwlknbij2 26242. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝑇⟶𝑊) | ||
Theorem | wlknwwlkninj 26239* | Lemma 2 for wlknwwlknbij2 26242. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1→𝑊) | ||
Theorem | wlknwwlknsur 26240* | Lemma 3 for wlknwwlknbij2 26242. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–onto→𝑊) | ||
Theorem | wlknwwlknbij 26241* | Lemma 4 for wlknwwlknbij2 26242. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1-onto→𝑊) | ||
Theorem | wlknwwlknbij2 26242* | There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → ∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁}–1-1-onto→((𝑉 WWalksN 𝐸)‘𝑁)) | ||
Theorem | wlknwwlknen 26243* | The set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁} ≈ ((𝑉 WWalksN 𝐸)‘𝑁)) | ||
Theorem | wlknwwlkneqs 26244* | The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → (#‘{𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁}) = (#‘((𝑉 WWalksN 𝐸)‘𝑁))) | ||
Theorem | wlkiswwlkfun 26245* | Lemma 1 for wlkiswwlkbij2 26249. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.) |
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)} & ⊢ 𝑊 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇⟶𝑊) | ||
Theorem | wlkiswwlkinj 26246* | Lemma 2 for wlkiswwlkbij2 26249. (Contributed by Alexander van der Vekens, 23-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.) |
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)} & ⊢ 𝑊 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1→𝑊) | ||
Theorem | wlkiswwlksur 26247* | Lemma 3 for wlkiswwlkbij2 26249. (Contributed by Alexander van der Vekens, 23-Jul-2018.) |
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)} & ⊢ 𝑊 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–onto→𝑊) | ||
Theorem | wlkiswwlkbij 26248* | Lemma 4 for wlkiswwlkbij2 26249. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)} & ⊢ 𝑊 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1-onto→𝑊) | ||
Theorem | wlkiswwlkbij2 26249* | There is a bijection between the set of walks of a fixed length, starting at a fixed vertex, and the set of walks represented as words of the same length, starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) | ||
Theorem | wwlkeq 26250* | Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018.) |
⊢ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ 𝑇 ∈ (𝑉 WWalks 𝐸)) → (𝑊 = 𝑇 ↔ ((#‘𝑊) = (#‘𝑇) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑇‘𝑖)))) | ||
Theorem | wwlknred 26251 | Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) |
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) | ||
Theorem | wwlknext 26252 | Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) |
⊢ ((𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) | ||
Theorem | wwlknextbi 26253 | Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018.) |
⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ 𝑊 = (𝑇 ++ 〈“𝑆”〉) ∧ {( lastS ‘𝑇), 𝑆} ∈ ran 𝐸)) → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ↔ 𝑇 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) | ||
Theorem | wwlknredwwlkn 26254* | For each walk (as word) of length at least 1 there is a shorter walk (as word). (Contributed by Alexander van der Vekens, 22-Aug-2018.) |
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) → ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸))) | ||
Theorem | wwlknredwwlkn0 26255* | For each walk (as word) of length at least 1 there is a shorter walk (as word) starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Aug-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1))) → ((𝑊‘0) = 𝑃 ↔ ∃𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)((𝑊 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑊)} ∈ ran 𝐸))) | ||
Theorem | wwlkextwrd 26256* | Lemma 0 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 5-Aug-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} ⇒ ⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) | ||
Theorem | wwlkextfun 26257* | Lemma 1 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 7-Aug-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷⟶𝑅) | ||
Theorem | wwlkextinj 26258* | Lemma 2 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 7-Aug-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐹:𝐷–1-1→𝑅) | ||
Theorem | wwlkextsur 26259* | Lemma 3 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 7-Aug-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) ⇒ ⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐹:𝐷–onto→𝑅) | ||
Theorem | wwlkextbij0 26260* | Lemma 4 for wwlkextbij 26261. (Contributed by Alexander van der Vekens, 7-Aug-2018.) |
⊢ 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = (𝑁 + 2) ∧ (𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)} & ⊢ 𝑅 = {𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ ( lastS ‘𝑡)) ⇒ ⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → 𝐹:𝐷–1-1-onto→𝑅) | ||
Theorem | wwlkextbij 26261* | There is a bijection between the extensions of a walk (as word) by an edge and the set of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 21-Aug-2018.) |
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}–1-1-onto→{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸}) | ||
Theorem | wwlkexthasheq 26262* | The number of the extensions of a walk (as word) by an edge equals the number of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 23-Aug-2018.) (Proof shortened by AV, 4-May-2021.) |
⊢ (𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ∣ ((𝑤 substr 〈0, (𝑁 + 1)〉) = 𝑊 ∧ {( lastS ‘𝑊), ( lastS ‘𝑤)} ∈ ran 𝐸)}) = (#‘{𝑛 ∈ 𝑉 ∣ {( lastS ‘𝑊), 𝑛} ∈ ran 𝐸})) | ||
Theorem | wwlkm1edg 26263 | Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018.) |
⊢ ((𝑊 ∈ (𝑉 WWalks 𝐸) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈ (𝑉 WWalks 𝐸)) | ||
Theorem | disjxwwlks 26264* | Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 29-Jul-2018.) |
⊢ Disj 𝑦 ∈ ((𝑉 WWalksN 𝐸)‘𝑁){𝑥 ∈ Word 𝑉 ∣ ((𝑥 substr 〈0, 𝑁〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)} | ||
Theorem | wwlknndef 26265 | Conditions for WWalksN not being defined. (Contributed by Alexander van der Vekens, 30-Jul-2018.) |
⊢ ((𝑉 ∉ V ∨ 𝐸 ∉ V ∨ 𝑁 ∉ ℕ0) → ((𝑉 WWalksN 𝐸)‘𝑁) = ∅) | ||
Theorem | wwlknfi 26266 | The number of walks represented by words of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 30-Jul-2018.) |
⊢ (𝑉 ∈ Fin → ((𝑉 WWalksN 𝐸)‘𝑁) ∈ Fin) | ||
Theorem | wlknfi 26267* | The number of walks of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑉 ∈ Fin) → {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st ‘𝑝)) = 𝑁} ∈ Fin) | ||
Theorem | wlknwwlknvbij 26268* | There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length and starting at the same vertex. (Contributed by Alexander van der Vekens, 30-Sep-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → ∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) | ||
Theorem | wwlkextproplem1 26269 | Lemma 1 for wwlkextprop 26272. (Contributed by Alexander van der Vekens, 31-Jul-2018.) |
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 substr 〈0, (𝑁 + 1)〉)‘0) = (𝑊‘0)) | ||
Theorem | wwlkextproplem2 26270 | Lemma 2 for wwlkextprop 26272. (Contributed by Alexander van der Vekens, 1-Aug-2018.) |
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {( lastS ‘(𝑊 substr 〈0, (𝑁 + 1)〉)), ( lastS ‘𝑊)} ∈ ran 𝐸) | ||
Theorem | wwlkextproplem3 26271* | Lemma 3 for wwlkextprop 26272. (Contributed by Alexander van der Vekens, 1-Aug-2018.) |
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) & ⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ (𝑊‘0) = 𝑃 ∧ 𝑁 ∈ ℕ0) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ 𝑌) | ||
Theorem | wwlkextprop 26272* | Adding additional properties to the set of walks (as words) of a fixed length starting at a fixed vertex. (Contributed by Alexander van der Vekens, 1-Aug-2018.) |
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) & ⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ (𝑁 ∈ ℕ0 → {𝑥 ∈ 𝑋 ∣ (𝑥‘0) = 𝑃} = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, (𝑁 + 1)〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)}) | ||
Theorem | disjxwwlkn 26273* | Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 21-Aug-2018.) |
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) & ⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ Disj 𝑦 ∈ 𝑌 {𝑥 ∈ 𝑋 ∣ ((𝑥 substr 〈0, 𝑀〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)} | ||
Theorem | hashwwlkext 26274* | Number of walks (as words) extended by an edge as sum over the prefixes. (Contributed by Alexander van der Vekens, 21-Aug-2018.) |
⊢ 𝑋 = ((𝑉 WWalksN 𝐸)‘(𝑁 + 1)) & ⊢ 𝑌 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ⇒ ⊢ (𝑉 ∈ Fin → (#‘{𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑌 ((𝑥 substr 〈0, 𝑀〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)}) = Σ𝑦 ∈ 𝑌 (#‘{𝑥 ∈ 𝑋 ∣ ((𝑥 substr 〈0, 𝑀〉) = 𝑦 ∧ (𝑦‘0) = 𝑃 ∧ {( lastS ‘𝑦), ( lastS ‘𝑥)} ∈ ran 𝐸)})) | ||
Syntax | cclwlk 26275 | Extend class notation with Closed Walks (of a graph). |
class ClWalks | ||
Syntax | cclwwlk 26276 | Extend class notation with Closed Walks (of a graph) as Word over the set of vertices. |
class ClWWalks | ||
Syntax | cclwwlkn 26277 | Extend class notation with Closed Walks (of a graph) of a fixed length as Word over the set of vertices. |
class ClWWalksN | ||
Definition | df-clwlk 26278* |
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 { 1 , ... , n } 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(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0). Notice that by this definition, a single vertex is a closed walk of length 0, see also 0clwlk 26293! (Contributed by Alexander van der Vekens, 12-Mar-2018.) |
⊢ ClWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Definition | df-clwwlk 26279* |
Define the set of all Closed Walks (in an undirected graph) as words
over the set of vertices. Such a word corresponds to the sequence p(0)
p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1)
e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlk 26278. Notice
that the word does not contain the terminating vertex p(n) of the walk,
because it is always equal to the first vertex of the closed walk.
Notice that by this definition, a single vertex cannot be represented as closed walk, since the word <" v "> with vertex v represents the walk "vv", which is a (closed) walk of length 1 (if there is an edge/loop from v to v). Therefore, a closed walk corresponds to a closed walk as word in an undirected graph only for walks of length at least 1, see clwlkisclwwlk2 26318. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
⊢ ClWWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝑒)}) | ||
Definition | df-clwwlkn 26280* | Define the set of all Closed Walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlk 26278. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
⊢ ClWWalksN = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑣 ClWWalks 𝑒) ∣ (#‘𝑤) = 𝑛})) | ||
Theorem | clwlk 26281* | The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ClWalks 𝐸) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓)))}) | ||
Theorem | isclwlk0 26282 | 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.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝑉 ClWalks 𝐸)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | isclwlkg 26283 | Generalisation of isclwlk0 26282: 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, 24-Jun-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹(𝑉 ClWalks 𝐸)𝑃 ↔ (𝐹(𝑉 Walks 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | isclwlk 26284* | Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝐹(𝑉 ClWalks 𝐸)𝑃 ↔ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))) | ||
Theorem | clwlkiswlk 26285 | A closed walk is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) |
⊢ (𝐹(𝑉 ClWalks 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) | ||
Theorem | clwlkswlks 26286 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
⊢ (𝑊 ∈ (𝑉 ClWalks 𝐸) → 𝑊 ∈ (𝑉 Walks 𝐸)) | ||
Theorem | clwlksarewlks 26287 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) |
⊢ (𝑉 ClWalks 𝐸) ⊆ (𝑉 Walks 𝐸) | ||
Theorem | wlkv0 26288 | If there is a walk in an empty graph, it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018.) |
⊢ (𝑊 ∈ (∅ Walks 𝐸) → ((1st ‘𝑊) = ∅ ∧ (2nd ‘𝑊) = ∅)) | ||
Theorem | wlk0 26289 | There is no walk in an empty graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.) |
⊢ (∅ Walks 𝐸) = ∅ | ||
Theorem | clwlk0 26290 | There is no closed walk in an empty graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.) |
⊢ (∅ ClWalks 𝐸) = ∅ | ||
Theorem | clwlkcomp 26291* | A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018.) |
⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (𝑉 ClWalks 𝐸) ↔ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))) | ||
Theorem | clwlkcompim 26292* | Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018.) |
⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (𝑉 ClWalks 𝐸) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | 0clwlk 26293 | A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 𝑃 ∈ 𝑍) → (∅(𝑉 ClWalks 𝐸)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | clwwlk 26294* | The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ClWWalks 𝐸) = {𝑤 ∈ Word 𝑉 ∣ (∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑤), (𝑤‘0)} ∈ ran 𝐸)}) | ||
Theorem | clwwlkn 26295* | The set of closed walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑉 ClWWalksN 𝐸)‘𝑁) = {𝑤 ∈ (𝑉 ClWWalks 𝐸) ∣ (#‘𝑤) = 𝑁}) | ||
Theorem | isclwwlk 26296* | Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑊 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸))) | ||
Theorem | isclwwlkn 26297 | Properties of a word to represent a closed walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ (𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘𝑊) = 𝑁))) | ||
Theorem | clwwlkprop 26298 | Properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) |
⊢ (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)) | ||
Theorem | clwwlkgt0 26299 | A closed walk in an undirected graph has a length of at least 2. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃))) | ||
Theorem | clwwlknprop 26300 | Properties of a closed walk of a fixed length as word. (Contributed by Alexander van der Vekens, 25-Mar-2018.) |
⊢ (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ 𝑃 ∈ Word 𝑉 ∧ (𝑁 ∈ ℕ0 ∧ (#‘𝑃) = 𝑁))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |