Home | Metamath
Proof Explorer Theorem List (p. 277 of 462) | < 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-28971) |
Hilbert Space Explorer
(28972-30494) |
Users' Mathboxes
(30495-46134) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vtxdginducedm1lem3 27601* | Lemma 3 for vtxdginducedm1 27603: an edge in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ (𝐻 ∈ 𝐼 → ((iEdg‘𝑆)‘𝐻) = (𝐸‘𝐻)) | ||
Theorem | vtxdginducedm1lem4 27602* | Lemma 4 for vtxdginducedm1 27603. (Contributed by AV, 17-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (𝑊 ∈ (𝑉 ∖ {𝑁}) → (♯‘{𝑘 ∈ 𝐽 ∣ (𝐸‘𝑘) = {𝑊}}) = 0) | ||
Theorem | vtxdginducedm1 27603* | The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 17-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) +𝑒 (♯‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)})) | ||
Theorem | vtxdginducedm1fi 27604* | The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 of finite size obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 18-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (𝐸 ∈ Fin → ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) + (♯‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)}))) | ||
Theorem | finsumvtxdg2ssteplem1 27605* | Lemma for finsumvtxdg2sstep 27609. (Contributed by AV, 15-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (♯‘𝐸) = ((♯‘𝑃) + (♯‘𝐽))) | ||
Theorem | finsumvtxdg2ssteplem2 27606* | Lemma for finsumvtxdg2sstep 27609. (Contributed by AV, 12-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘𝐽) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) | ||
Theorem | finsumvtxdg2ssteplem3 27607* | Lemma for finsumvtxdg2sstep 27609. (Contributed by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(♯‘{𝑖 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑖)}) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (♯‘𝐽)) | ||
Theorem | finsumvtxdg2ssteplem4 27608* | Lemma for finsumvtxdg2sstep 27609. (Contributed by AV, 12-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (♯‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((♯‘𝐽) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) = (2 · ((♯‘𝑃) + (♯‘𝐽)))) | ||
Theorem | finsumvtxdg2sstep 27609* | Induction step of finsumvtxdg2size 27610: In a finite pseudograph of finite size, the sum of the degrees of all vertices of the pseudograph is twice the size of the pseudograph if the sum of the degrees of all vertices of the subgraph of the pseudograph not containing one of the vertices is twice the size of the subgraph. (Contributed by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((𝑃 ∈ Fin → Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (♯‘𝑃))) → Σ𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = (2 · (♯‘𝐸)))) | ||
Theorem | finsumvtxdg2size 27610* |
The sum of the degrees of all vertices of a finite pseudograph of finite
size is twice the size of the pseudograph. See equation (1) in section
I.1 in [Bollobas] p. 4. Here, the
"proof" is simply the statement
"Since each edge has two endvertices, the sum of the degrees is
exactly
twice the number of edges". The formal proof of this theorem (for
pseudographs) is much more complicated, taking also the used auxiliary
theorems into account. The proof for a (finite) simple graph (see
fusgr1th 27611) would be shorter, but nevertheless still
laborious.
Although this theorem would hold also for infinite pseudographs and
pseudographs of infinite size, the proof of this most general version
(see theorem "sumvtxdg2size" below) would require many more
auxiliary
theorems (e.g., the extension of the sum Σ
over an arbitrary
set).
I dedicate this theorem and its proof to Norman Megill, who deceased too early on December 9, 2021. This proof is an example for the rigor which was the main motivation for Norman Megill to invent and develop Metamath, see section 1.1.6 "Rigor" on page 19 of the Metamath book: "... it is usually assumed in mathematical literature that the person reading the proof is a mathematician familiar with the specialty being described, and that the missing steps are obvious to such a reader or at least the reader is capable of filling them in." I filled in the missing steps of Bollobas' proof as Norm would have liked it... (Contributed by Alexander van der Vekens, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼))) | ||
Theorem | fusgr1th 27611* | The sum of the degrees of all vertices of a finite simple graph is twice the size of the graph. See equation (1) in section I.1 in [Bollobas] p. 4. Also known as the "First Theorem of Graph Theory" (see https://charlesreid1.com/wiki/First_Theorem_of_Graph_Theory). (Contributed by AV, 26-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼))) | ||
Theorem | finsumvtxdgeven 27612* | The sum of the degrees of all vertices of a finite pseudograph of finite size is even. See equation (2) in section I.1 in [Bollobas] p. 4, where it is also called the handshaking lemma. (Contributed by AV, 22-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → 2 ∥ Σ𝑣 ∈ 𝑉 (𝐷‘𝑣)) | ||
Theorem | vtxdgoddnumeven 27613* | The number of vertices of odd degree is even in a finite pseudograph of finite size. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 22-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → 2 ∥ (♯‘{𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ (𝐷‘𝑣)})) | ||
Theorem | fusgrvtxdgonume 27614* | The number of vertices of odd degree is even in a finite simple graph. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 27-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → 2 ∥ (♯‘{𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ (𝐷‘𝑣)})) | ||
With df-rgr 27617 and df-rusgr 27618, k-regularity of a (simple) graph is defined as predicate RegGraph resp. RegUSGraph. Instead of defining a predicate, an alternative could have been to define a function that maps an extended nonnegative integer to the class of "graphs" in which every vertex has the extended nonnegative integer as degree: RegGraph = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘}). This function, however, would not be defined at least for 𝑘 = 0 (see rgrx0nd 27654), because {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} is not a set (see rgrprcx 27652). It is expected that this function is not defined for every 𝑘 ∈ ℕ0* (how could this be proven?). | ||
Syntax | crgr 27615 | Extend class notation to include the class of all regular graphs. |
class RegGraph | ||
Syntax | crusgr 27616 | Extend class notation to include the class of all regular simple graphs. |
class RegUSGraph | ||
Definition | df-rgr 27617* | Define the "k-regular" predicate, which is true for a "graph" being k-regular: read 𝐺 RegGraph 𝐾 as "𝐺 is 𝐾-regular" or "𝐺 is a 𝐾-regular graph". Note that 𝐾 is allowed to be positive infinity (𝐾 ∈ ℕ0*), as proposed by GL. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ RegGraph = {〈𝑔, 𝑘〉 ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)} | ||
Definition | df-rusgr 27618* | Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read 𝐺 RegUSGraph 𝐾 as 𝐺 is a 𝐾-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ RegUSGraph = {〈𝑔, 𝑘〉 ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)} | ||
Theorem | isrgr 27619* | The property of a class being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGraph 𝐾 ↔ (𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))) | ||
Theorem | rgrprop 27620* | The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 RegGraph 𝐾 → (𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)) | ||
Theorem | isrusgr 27621 | The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾))) | ||
Theorem | rusgrprop 27622 | The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾)) | ||
Theorem | rusgrrgr 27623 | A k-regular simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 RegGraph 𝐾) | ||
Theorem | rusgrusgr 27624 | A k-regular simple graph is a simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph) | ||
Theorem | finrusgrfusgr 27625 | A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph) | ||
Theorem | isrusgr0 27626* | The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))) | ||
Theorem | rusgrprop0 27627* | The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)) | ||
Theorem | usgreqdrusgr 27628* | If all vertices in a simple graph have the same degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾) → 𝐺 RegUSGraph 𝐾) | ||
Theorem | fusgrregdegfi 27629* | In a nonempty finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.) (Revised by AV, 19-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 → 𝐾 ∈ ℕ0)) | ||
Theorem | fusgrn0eqdrusgr 27630* | If all vertices in a nonempty finite simple graph have the same (finite) degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 → 𝐺 RegUSGraph 𝐾)) | ||
Theorem | frusgrnn0 27631 | In a nonempty finite k-regular simple graph, the degree of each vertex is finite. (Contributed by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈ ℕ0) | ||
Theorem | 0edg0rgr 27632 | A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (iEdg‘𝐺) = ∅) → 𝐺 RegGraph 0) | ||
Theorem | uhgr0edg0rgr 27633 | A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ (Edg‘𝐺) = ∅) → 𝐺 RegGraph 0) | ||
Theorem | uhgr0edg0rgrb 27634 | A hypergraph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.) |
⊢ (𝐺 ∈ UHGraph → (𝐺 RegGraph 0 ↔ (Edg‘𝐺) = ∅)) | ||
Theorem | usgr0edg0rusgr 27635 | A simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 19-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
⊢ (𝐺 ∈ USGraph → (𝐺 RegUSGraph 0 ↔ (Edg‘𝐺) = ∅)) | ||
Theorem | 0vtxrgr 27636* | A null graph (with no vertices) is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegGraph 𝑘) | ||
Theorem | 0vtxrusgr 27637* | A graph with no vertices and an empty edge function is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘) | ||
Theorem | 0uhgrrusgr 27638* | The null graph as hypergraph is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘) | ||
Theorem | 0grrusgr 27639 | The null graph represented by an empty set is a k-regular simple graph for every k. (Contributed by AV, 26-Dec-2020.) |
⊢ ∀𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘 | ||
Theorem | 0grrgr 27640 | The null graph represented by an empty set is k-regular for every k. (Contributed by AV, 26-Dec-2020.) |
⊢ ∀𝑘 ∈ ℕ0* ∅ RegGraph 𝑘 | ||
Theorem | cusgrrusgr 27641 | A complete simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝐺 RegUSGraph ((♯‘𝑉) − 1)) | ||
Theorem | cusgrm1rusgr 27642 | A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for 𝑘 ∈ ℤ, then the assumption 𝑉 ≠ ∅ could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ((♯‘𝑉) − 1))) | ||
Theorem | rusgrpropnb 27643* | The properties of a k-regular simple graph expressed with neighbors. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘(𝐺 NeighbVtx 𝑣)) = 𝐾)) | ||
Theorem | rusgrpropedg 27644* | The properties of a k-regular simple graph expressed with edges. (Contributed by AV, 23-Dec-2020.) (Revised by AV, 27-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘{𝑒 ∈ (Edg‘𝐺) ∣ 𝑣 ∈ 𝑒}) = 𝐾)) | ||
Theorem | rusgrpropadjvtx 27645* | The properties of a k-regular simple graph expressed with adjacent vertices. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 27-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘{𝑘 ∈ 𝑉 ∣ {𝑣, 𝑘} ∈ (Edg‘𝐺)}) = 𝐾)) | ||
Theorem | rusgrnumwrdl2 27646* | In a k-regular simple graph, the number of edges resp. walks of length 1 (represented as words of length 2) starting at a fixed vertex is k. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 6-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))}) = 𝐾) | ||
Theorem | rusgr1vtxlem 27647* | Lemma for rusgr1vtx 27648. (Contributed by AV, 27-Dec-2020.) |
⊢ (((∀𝑣 ∈ 𝑉 (♯‘𝐴) = 𝐾 ∧ ∀𝑣 ∈ 𝑉 𝐴 = ∅) ∧ (𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 1)) → 𝐾 = 0) | ||
Theorem | rusgr1vtx 27648 | If a k-regular simple graph has only one vertex, then k must be 0. (Contributed by Alexander van der Vekens, 4-Sep-2018.) (Revised by AV, 27-Dec-2020.) |
⊢ (((♯‘(Vtx‘𝐺)) = 1 ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 = 0) | ||
Theorem | rgrusgrprc 27649* | The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ {𝑔 ∈ USGraph ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V | ||
Theorem | rusgrprc 27650 | The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ {𝑔 ∣ 𝑔 RegUSGraph 0} ∉ V | ||
Theorem | rgrprc 27651 | The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ {𝑔 ∣ 𝑔 RegGraph 0} ∉ V | ||
Theorem | rgrprcx 27652* | The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V | ||
Theorem | rgrx0ndm 27653* | 0 is not in the domain of the potentially alternative definition of the sets of k-regular graphs for each extended nonnegative integer k. (Contributed by AV, 28-Dec-2020.) |
⊢ 𝑅 = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘}) ⇒ ⊢ 0 ∉ dom 𝑅 | ||
Theorem | rgrx0nd 27654* | The potentially alternatively defined k-regular graphs is not defined for k=0. (Contributed by AV, 28-Dec-2020.) |
⊢ 𝑅 = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘}) ⇒ ⊢ (𝑅‘0) = ∅ | ||
A "walk" in a graph is usually defined for simple graphs, multigraphs or even pseudographs as "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, or "A walk (of length k) in a graph is a nonempty alternating sequence v0 e0 v1 e1 ... e(k-1) vk of vertices and edges in G such that ei = { vi , vi+1 } for all i < k.", see definition of [Diestel] p. 10. Formalizing these definitions (mainly by representing the indexed vertices and edges by functions), a walk is represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges (e is a third function enumerating the edges within the graph, not within the walk), and p enumerates the vertices, see df-wlks 27659. Hence a walk (of length n) is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Alternatively, one could define a walk as a function 𝑤:(0...(2 · 𝑛))⟶((Edg‘𝐺) ∪ (Vtx‘𝐺)) such that for all 0 ≤ 𝑘 ≤ 𝑛, (𝑤‘(2 · 𝑘)) ∈ (Vtx‘𝐺) and for all 0 ≤ 𝑘 ≤ (𝑛 − 1), (𝑤‘((2 · 𝑘) + 1)) ∈ (Edg‘𝐺) and {(𝑤‘(2 · 𝑘)), (𝑤‘((2 · 𝑘) + 2))} ⊆ (𝑤‘((2 · 𝑘) + 1)). Based on our definition of Walks, the class of all walks, more restrictive constructs are defined: * Trails (df-trls 27752): A "walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5, i.e., f(i) =/= f(j) if i =/= j. * Paths (df-pths 27775): A path is a walk whose vertices except the first and the last vertex are distinct, i.e., p(i) =/= p(j) if i < j, except possibly when i = 0 and j = n. * SPaths (simple paths, df-spths 27776): A simple path "is a walk with distinct vertices.", see Notation of [Bollobas] p. 5, i.e., p(i) =/= p(j) if i =/= j. * ClWalks (closed walks, df-clwlks 27830): A walk whose endvertices coincide is called a closed walk, i.e., p(0) = p(n). * Circuits (df-crcts 27845): "A trail whose endvertices coincide (a closed trail) is called a circuit." (see Definition of [Bollobas] p. 5), i.e., f(i) =/= f(j) if i =/= j and p(0) = p(n). Equivalently, a circuit is a closed walk with distinct edges. * Cycles (df-cycls 27846): A path whose endvertices coincide (a closed path) is called a cycle, i.e., p(i) =/= p(j) if i =/= j, except i = 0 and j = n, and p(0) = p(n). Equivalently, a cycle is a closed walk with distinct vertices. * EulerPaths (Eulerian paths, df-eupth 28253): An Eulerian path is "a trail containing all edges [of the graph]" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Note, however, that an Eulerian path needs not be a path. * Eulerian circuit: An Eulerian circuit (called Euler tour in the definition in [Diestel] p. 22) is "a circuit in a graph containing all the edges" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j, p(0) = p(n) and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Hierarchy of all kinds of walks (apply ssriv 3895 and elopabran 5431 to the mentioned theorems to obtain the following subset relationships, as available for clwlkiswlk 27833, see clwlkwlk 27834 and clwlkswks 27835): * Trails are walks (trliswlk 27757): (Trails‘𝐺) ⊆ (Walks‘𝐺) * Paths are trails (pthistrl 27784): (Paths‘𝐺) ⊆ (Trails‘𝐺) * Simple paths are paths (spthispth 27785): (SPaths‘𝐺) ⊆ (Paths‘𝐺) * Closed walks are walks (clwlkiswlk 27833): (ClWalks‘𝐺) ⊆ (Walks‘𝐺) * Circuits are closed walks (crctisclwlk 27853): (Circuits‘𝐺) ⊆ (ClWalks‘𝐺) * Circuits are trails (crctistrl 27854): (Circuits‘𝐺) ⊆ (Trails‘𝐺) * Cycles are paths (cyclispth 27856): (Cycles‘𝐺) ⊆ (Paths‘𝐺) * Cycles are circuits (cycliscrct 27858): (Cycles‘𝐺) ⊆ (Circuits‘𝐺) * (Non-trivial) cycles are not simple paths (cyclnspth 27859): (𝐹 ≠ ∅ → (𝐹(Cycles‘𝐺)𝑃 → ¬ 𝐹(SPaths‘𝐺)𝑃)) * Eulerian paths are trails (eupthistrl 28266): (EulerPaths‘𝐺) ⊆ (Trails‘𝐺) Often, it is sufficient to refer to a walk by the natural sequence of its vertices, i.e., omitting its edges in its representation: p(0) p(1) ... p(n-1) p(n), see the corresponding remark in [Diestel] p. 6. The concept of a Word, see df-word 14053, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in definition df-wwlks 27886 for WWalks, and the representation of a walk as sequence of its vertices is called "walk as word". Only for simple pseudographs, however, the edges can be uniquely reconstructed from such a representation. In this case, the general definitions of walks and the definition of walks as words are equivalent, see wlkiswwlks 27932. In other cases, there could be more than one edge between two adjacent vertices in the walk (in a multigraph), or two adjacent vertices could be connected by two different hyperedges involving additional vertices (in a hypergraph). Based on this definition of WWalks, the class of all walks as word, more restrictive constructs are defined analogously to the general definition of a walk: * WWalksN (walks of length N as word, df-wwlksn 27887): n = N * WSPathsN (simple paths of length N as word, df-wspthsn 27889): p(i) =/= p(j) if i =/= j and n = N * ClWWalks (closed walks as word, df-clwwlk 28037): p(0) = p(n) * ClWWalksN (closed walks of length N as word, df-clwwlkn 28080): p(0) = p(n) and n = N Finally, there are a couple of definitions for (special) walks 〈𝐹, 𝑃〉 having fixed endpoints 𝐴 and 𝐵: * Walks with particular endpoints (df-wlkson 27660): 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 * Trails with particular endpoints (df-trlson 27753): 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 * Paths with particular endpoints (df-pthson 27777): 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 * Simple paths with particular endpoints (df-spthson 27778): 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 * Walks of a fixed length 𝑁 as words with particular endpoints (df-wwlksnon 27888): (𝐴(𝑁 WWalksNOn 𝐺)𝐵) * Simple paths of a fixed length 𝑁 as words with particular endpoints (df-wspthsnon 27890): (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) * Closed Walks of a fixed length 𝑁 as words anchored at a particular vertex 𝐴 (df-wwlksnon 27888): (𝐴(ClWWalksNOn‘𝐺)𝑁) | ||
A "walk" within a graph is usually defined for simple graphs, multigraphs or even pseudographs as "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. This definition requires the edges to connect two vertices at most (loops are also allowed: if e(i) is a loop, then x(i-1) = x(i)). For hypergraphs containing hyperedges (i.e. edges connecting more than two vertices), however, a more general definition is needed. Two approaches for a definition applicable for arbitrary hypergraphs are used in the literature: "walks on the vertex level" and "walks on the edge level" (see Aksoy, Joslyn, Marrero, Praggastis, Purvine: "Hypernetwork science via high-order hypergraph walks", June 2020, https://doi.org/10.1140/epjds/s13688-020-00231-0): "walks on the edge level": For a positive integer s, an s-walk of length k between hyperedges f and g is a sequence of hyperedges, f=e(0), e(1), ... , e(k)=g, where for j=1, ... , k, e(j-1) =/= e(j) and e(j-1) and e(j) have at least s vertices in common (according to Aksoy et al.). "walks on the vertex level": For a positive integer s, an s-walk of length k between vertices a and b is a sequence of vertices, a=v(0), v(1), ... , v(k)=b, where for j=1, ... , k, v(j-1) and v(j) are connected by at least s edges (analogous to Aksoy et al.). There are two imperfections for the definition for "walks on the edge level": one is that a walk of length 1 consists of two edges (or a walk of length 0 consists of one edge), whereas a walk of length 1 on the vertex level consists of two vertices and one edge (or a walk of length 0 consists of one vertex and no edge). The other is that edges, especially loops, can be traversed only once (and not repeatedly) because of the condition e(j-1) =/= e(j). The latter is avoided in the definition for EdgWalks, see df-ewlks 27658. To be compatible with the (usual) definition of walks for pseudographs, walks also suitable for arbitrary hypergraphs are defined "on the vertex level" in the following as Walks, see df-wlks 27659, restricting s to 1. wlk1ewlk 27699 shows that such a 1-walk "on the vertex level" induces a 1-walk "on the edge level". | ||
Syntax | cewlks 27655 | Extend class notation with s-walks "on the edge level" (of a hypergraph). |
class EdgWalks | ||
Syntax | cwlks 27656 | Extend class notation with walks (i.e. 1-walks) (of a hypergraph). |
class Walks | ||
Syntax | cwlkson 27657 | Extend class notation with walks between two vertices (within a graph). |
class WalksOn | ||
Definition | df-ewlks 27658* | Define the set of all s-walks of edges (in a hypergraph) corresponding to s-walks "on the edge level" discussed in Aksoy et al. For an extended nonnegative integer s, an s-walk is a sequence of hyperedges, e(0), e(1), ... , e(k), where e(j-1) and e(j) have at least s vertices in common (for j=1, ... , k). In contrast to the definition in Aksoy et al., 𝑠 = 0 (a 0-walk is an arbitrary sequence of hyperedges) and 𝑠 = +∞ (then the number of common vertices of two adjacent hyperedges must be infinite) are allowed. Furthermore, it is not forbidden that adjacent hyperedges are equal. (Contributed by AV, 4-Jan-2021.) |
⊢ EdgWalks = (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))}) | ||
Definition | df-wlks 27659* |
Define the set of all walks (in a hypergraph). Such walks correspond to
the s-walks "on the vertex level" (with s = 1), and also to
1-walks "on
the edge level" (see wlk1walk 27698) discussed in Aksoy et al. The
predicate 𝐹(Walks‘𝐺)𝑃 can be read as "The pair
〈𝐹, 𝑃〉 represents a walk in a graph
𝐺", see also iswlk 27670.
The condition {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘)) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. (𝑝‘𝑘) = (𝑝‘(𝑘 + 1)) should be allowed only if there is a loop at (𝑝‘𝑘). Otherwise, C would be fulfilled by each edge containing (𝑝‘𝑘). According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", 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 AV, 30-Dec-2020.) |
⊢ Walks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))}) | ||
Definition | df-wlkson 27660* | Define the collection of walks with particular endpoints (in a hypergraph). The predicate 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 can be read as "The pair 〈𝐹, 𝑃〉 represents a walk from vertex 𝐴 to vertex 𝐵 in a graph 𝐺", see also iswlkon 27717. 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.) (Revised by AV, 28-Dec-2020.) |
⊢ WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)})) | ||
Theorem | ewlksfval 27661* | The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*) → (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑆 ≤ (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))}) | ||
Theorem | isewlk 27662* | Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈) → (𝐹 ∈ (𝐺 EdgWalks 𝑆) ↔ (𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘))))))) | ||
Theorem | ewlkprop 27663* | Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | ewlkinedg 27664 | The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝐾 ∈ (1..^(♯‘𝐹))) → 𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝐾 − 1))) ∩ (𝐼‘(𝐹‘𝐾))))) | ||
Theorem | ewlkle 27665 | An s-walk of edges is also a t-walk of edges if 𝑡 ≤ 𝑠. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆) → 𝐹 ∈ (𝐺 EdgWalks 𝑇)) | ||
Theorem | upgrewlkle2 27666 | In a pseudograph, there is no s-walk of edges of length greater than 1 with s>2. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 1 < (♯‘𝐹)) → 𝑆 ≤ 2) | ||
Theorem | wkslem1 27667 | Lemma 1 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.) |
⊢ (𝐴 = 𝐵 → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘(𝐵 + 1)), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘(𝐵 + 1))} ⊆ (𝐼‘(𝐹‘𝐵))))) | ||
Theorem | wkslem2 27668 | Lemma 2 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.) |
⊢ ((𝐴 = 𝐵 ∧ (𝐴 + 1) = 𝐶) → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘𝐶), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘𝐶)} ⊆ (𝐼‘(𝐹‘𝐵))))) | ||
Theorem | wksfval 27669* | The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (Walks‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))}) | ||
Theorem | iswlk 27670* | Properties of a pair of functions to be a walk. (Contributed by AV, 30-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | wlkprop 27671* | Properties of a walk. (Contributed by AV, 5-Nov-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) | ||
Theorem | wlkv 27672 | The classes involved in a walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.) |
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) | ||
Theorem | iswlkg 27673* | Generalization of iswlk 27670: Conditions for two classes to represent a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | wlkf 27674 | The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) | ||
Theorem | wlkcl 27675 | A walk has length ♯(𝐹), which is an integer. Formerly proven for an Eulerian path, see eupthcl 28265. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ0) | ||
Theorem | wlkp 27676 | The mapping enumerating the vertices of a walk is a function. (Contributed by AV, 5-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) | ||
Theorem | wlkpwrd 27677 | The sequence of vertices of a walk is a word over the set of vertices. (Contributed by AV, 27-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃 ∈ Word 𝑉) | ||
Theorem | wlklenvp1 27678 | The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.) |
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝑃) = ((♯‘𝐹) + 1)) | ||
Theorem | wksv 27679* | The class of walks is a set. (Contributed by AV, 15-Jan-2021.) |
⊢ {〈𝑓, 𝑝〉 ∣ 𝑓(Walks‘𝐺)𝑝} ∈ V | ||
Theorem | wlkn0 27680 | The sequence 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.) (Revised by AV, 2-Jan-2021.) |
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃 ≠ ∅) | ||
Theorem | wlklenvm1 27681 | The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) = ((♯‘𝑃) − 1)) | ||
Theorem | ifpsnprss 27682 | Lemma for wlkvtxeledg 27683: Two adjacent (not necessarily different) vertices 𝐴 and 𝐵 in a walk are incident with an edge 𝐸. (Contributed by AV, 4-Apr-2021.) (Revised by AV, 5-Nov-2021.) |
⊢ (if-(𝐴 = 𝐵, 𝐸 = {𝐴}, {𝐴, 𝐵} ⊆ 𝐸) → {𝐴, 𝐵} ⊆ 𝐸) | ||
Theorem | wlkvtxeledg 27683* | Each pair of adjacent vertices in a walk is a subset of an edge. (Contributed by AV, 28-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) | ||
Theorem | wlkvtxiedg 27684* | The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(♯‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) | ||
Theorem | relwlk 27685 | The set (Walks‘𝐺) of all walks on 𝐺 is a set of pairs by our definition of a walk, and so is a relation. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 19-Feb-2021.) |
⊢ Rel (Walks‘𝐺) | ||
Theorem | wlkvv 27686 | If there is at least one walk in the graph, all walks are in the universal class of ordered pairs. (Contributed by AV, 2-Jan-2021.) |
⊢ ((1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊) → 𝑊 ∈ (V × V)) | ||
Theorem | wlkop 27687 | A walk is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 1-Jan-2021.) |
⊢ (𝑊 ∈ (Walks‘𝐺) → 𝑊 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) | ||
Theorem | wlkcpr 27688 | A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ (𝑊 ∈ (Walks‘𝐺) ↔ (1st ‘𝑊)(Walks‘𝐺)(2nd ‘𝑊)) | ||
Theorem | wlk2f 27689* | If there is a walk 𝑊 there is a pair of functions representing this walk. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ (𝑊 ∈ (Walks‘𝐺) → ∃𝑓∃𝑝 𝑓(Walks‘𝐺)𝑝) | ||
Theorem | wlkcomp 27690* | A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (Walks‘𝐺) ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | wlkcompim 27691* | Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (Walks‘𝐺) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) | ||
Theorem | wlkelwrd 27692 | The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (Walks‘𝐺) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉)) | ||
Theorem | wlkeq 27693* | Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.) (Revised by AV, 14-Apr-2021.) |
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺) ∧ 𝑁 = (♯‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) | ||
Theorem | edginwlk 27694 | The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 9-Dec-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼 ∧ 𝐾 ∈ (0..^(♯‘𝐹))) → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸) | ||
Theorem | upgredginwlk 27695 | The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom 𝐼) → (𝐾 ∈ (0..^(♯‘𝐹)) → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸)) | ||
Theorem | iedginwlk 27696 | The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 23-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((Fun 𝐼 ∧ 𝐹(Walks‘𝐺)𝑃 ∧ 𝑋 ∈ (0..^(♯‘𝐹))) → (𝐼‘(𝐹‘𝑋)) ∈ ran 𝐼) | ||
Theorem | wlkl1loop 27697 | A walk of length 1 from a vertex to itself is a loop. (Contributed by AV, 23-Apr-2021.) |
⊢ (((Fun (iEdg‘𝐺) ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} ∈ (Edg‘𝐺)) | ||
Theorem | wlk1walk 27698* | A walk is a 1-walk "on the edge level" according to Aksoy et al. (Contributed by AV, 30-Dec-2020.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (1..^(♯‘𝐹))1 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘))))) | ||
Theorem | wlk1ewlk 27699 | A walk is an s-walk "on the edge level" (with s=1) according to Aksoy et al. (Contributed by AV, 5-Jan-2021.) |
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ (𝐺 EdgWalks 1)) | ||
Theorem | upgriswlk 27700* | Properties of a pair of functions to be a walk in a pseudograph. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 28-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |