Home | Metamath
Proof Explorer Theorem List (p. 290 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3wlkond 28901 | A walk of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (π β πΉ(π΄(WalksOnβπΊ)π·)π) | ||
Theorem | 3trld 28902 | Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) β β’ (π β πΉ(TrailsβπΊ)π) | ||
Theorem | 3trlond 28903 | A trail of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) β β’ (π β πΉ(π΄(TrailsOnβπΊ)π·)π) | ||
Theorem | 3pthd 28904 | A path of length 3 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) β β’ (π β πΉ(PathsβπΊ)π) | ||
Theorem | 3pthond 28905 | A path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) β β’ (π β πΉ(π΄(PathsOnβπΊ)π·)π) | ||
Theorem | 3spthd 28906 | A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) & β’ (π β π΄ β π·) β β’ (π β πΉ(SPathsβπΊ)π) | ||
Theorem | 3spthond 28907 | A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) & β’ (π β π΄ β π·) β β’ (π β πΉ(π΄(SPathsOnβπΊ)π·)π) | ||
Theorem | 3cycld 28908 | Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) & β’ (π β π΄ = π·) β β’ (π β πΉ(CyclesβπΊ)π) | ||
Theorem | 3cyclpd 28909 | Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
β’ π = β¨βπ΄π΅πΆπ·ββ© & β’ πΉ = β¨βπ½πΎπΏββ© & β’ (π β ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π))) & β’ (π β ((π΄ β π΅ β§ π΄ β πΆ) β§ (π΅ β πΆ β§ π΅ β π·) β§ πΆ β π·)) & β’ (π β ({π΄, π΅} β (πΌβπ½) β§ {π΅, πΆ} β (πΌβπΎ) β§ {πΆ, π·} β (πΌβπΏ))) & β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β (π½ β πΎ β§ π½ β πΏ β§ πΎ β πΏ)) & β’ (π β π΄ = π·) β β’ (π β (πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 3 β§ (πβ0) = π΄)) | ||
Theorem | upgr3v3e3cycl 28910* | If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
β’ πΈ = (EdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 3) β βπ β π βπ β π βπ β π (({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π β§ π β π))) | ||
Theorem | uhgr3cyclexlem 28911 | Lemma for uhgr3cyclex 28912. (Contributed by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((((π΄ β π β§ π΅ β π) β§ π΄ β π΅) β§ ((π½ β dom πΌ β§ {π΅, πΆ} = (πΌβπ½)) β§ (πΎ β dom πΌ β§ {πΆ, π΄} = (πΌβπΎ)))) β π½ β πΎ) | ||
Theorem | uhgr3cyclex 28912* | If there are three different vertices in a hypergraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UHGraph β§ ((π΄ β π β§ π΅ β π β§ πΆ β π) β§ (π΄ β π΅ β§ π΄ β πΆ β§ π΅ β πΆ)) β§ ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ β§ {πΆ, π΄} β πΈ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄)) | ||
Theorem | umgr3cyclex 28913* | If there are three (different) vertices in a multigraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UMGraph β§ (π΄ β π β§ π΅ β π β§ πΆ β π) β§ ({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ β§ {πΆ, π΄} β πΈ)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π΄)) | ||
Theorem | umgr3v3e3cycl 28914* | If and only if there is a 3-cycle in a multigraph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β UMGraph β (βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ))) | ||
Theorem | upgr4cycl4dv4e 28915* | If there is a cycle of length 4 in a pseudograph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 13-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 4) β βπ β π βπ β π βπ β π βπ β π ((({π, π} β πΈ β§ {π, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π} β πΈ)) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) | ||
Syntax | cconngr 28916 | Extend class notation with connected graphs. |
class ConnGraph | ||
Definition | df-conngr 28917* | Define the class of all connected graphs. A graph is called connected if there is a path between every pair of (distinct) vertices. The distinctness of the vertices is not necessary for the definition, because there is always a path (of length 0) from a vertex to itself, see 0pthonv 28859 and dfconngr1 28918. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ConnGraph = {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β π£ βπβπ π(π(PathsOnβπ)π)π} | ||
Theorem | dfconngr1 28918* | Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ConnGraph = {π β£ [(Vtxβπ) / π£]βπ β π£ βπ β (π£ β {π})βπβπ π(π(PathsOnβπ)π)π} | ||
Theorem | isconngr 28919* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (πΊ β ConnGraph β βπ β π βπ β π βπβπ π(π(PathsOnβπΊ)π)π)) | ||
Theorem | isconngr1 28920* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β π β (πΊ β ConnGraph β βπ β π βπ β (π β {π})βπβπ π(π(PathsOnβπΊ)π)π)) | ||
Theorem | cusconngr 28921 | A complete hypergraph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ((πΊ β UHGraph β§ πΊ β ComplGraph) β πΊ β ConnGraph) | ||
Theorem | 0conngr 28922 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ β β ConnGraph | ||
Theorem | 0vconngr 28923 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β ) β πΊ β ConnGraph) | ||
Theorem | 1conngr 28924 | A graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
β’ ((πΊ β π β§ (VtxβπΊ) = {π}) β πΊ β ConnGraph) | ||
Theorem | conngrv2edg 28925* | A vertex in a connected graph with more than one vertex is incident with at least one edge. Formerly part of proof for vdgn0frgrv2 29025. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β ConnGraph β§ π β π β§ 1 < (β―βπ)) β βπ β ran πΌ π β π) | ||
Theorem | vdn0conngrumgrv2 28926 | A vertex in a connected multigraph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (((πΊ β ConnGraph β§ πΊ β UMGraph) β§ (π β π β§ 1 < (β―βπ))) β ((VtxDegβπΊ)βπ) β 0) | ||
According to Wikipedia ("Eulerian path", 9-Mar-2021, https://en.wikipedia.org/wiki/Eulerian_path): "In graph theory, an Eulerian trail (or Eulerian path) is a trail in a finite graph that visits every edge exactly once (allowing for revisiting vertices). Similarly, an Eulerian circuit or Eulerian cycle is an Eulerian trail that starts and ends on the same vertex. ... The term Eulerian graph has two common meanings in graph theory. One meaning is a graph with an Eulerian circuit, and the other is a graph with every vertex of even degree. These definitions coincide for connected graphs. ... A graph that has an Eulerian trail but not an Eulerian circuit is called semi-Eulerian." Correspondingly, an Eulerian path is defined as "a trail containing all edges" (see definition in [Bollobas] p. 16) in df-eupth 28928 resp. iseupth 28931. (EulerPathsβπΊ) is the set of all Eulerian paths in graph πΊ, see eupths 28930. 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), or, with other words, a circuit which is an Eulerian path. The function mapping a graph to the set of its Eulerian paths is defined as EulerPaths in df-eupth 28928, whereas there is no explicit definition for Eulerian circuits (yet): The statement "β¨πΉ, πβ© is an Eulerian circuit" is formally expressed by (πΉ(EulerPathsβπΊ)π β§ πΉ(CircuitsβπΊ)π). Each Eulerian path can be made an Eulerian circuit by adding an edge which connects the endpoints of the Eulerian path (see eupth2eucrct 28947). Vice versa, removing one edge from a graph with an Eulerian circuit results in a graph with an Eulerian path, see eucrct2eupth 28975. An Eulerian path does not have to be a path in the meaning of definition df-pths 28450, because it may traverse some vertices more than once. Therefore, "Eulerian trail" would be a more appropriate name. The main result of this section is (one direction of) Euler's Theorem: "A non-trivial connected graph has an Euler[ian] circuit iff each vertex has even degree." (see part 1 of theorem 12 in [Bollobas] p. 16 and theorem 1.8.1 in [Diestel] p. 22) or, expressed with Eulerian paths: "A connected graph has an Euler[ian] trail from a vertex x to a vertex y (not equal with x) iff x and y are the only vertices of odd degree." (see part 2 of theorem 12 in [Bollobas] p. 17). In eulerpath 28971, it is shown that a pseudograph with an Eulerian path has either zero or two vertices of odd degree, and eulercrct 28972 shows that a pseudograph with an Eulerian circuit has only vertices of even degree. | ||
Syntax | ceupth 28927 | Extend class notation with Eulerian paths. |
class EulerPaths | ||
Definition | df-eupth 28928* | Define the set of all Eulerian paths on an arbitrary graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ EulerPaths = (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ π:(0..^(β―βπ))βontoβdom (iEdgβπ))}) | ||
Theorem | releupth 28929 | The set (EulerPathsβπΊ) of all Eulerian paths on πΊ is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ Rel (EulerPathsβπΊ) | ||
Theorem | eupths 28930* | The Eulerian paths on the graph πΊ. (Contributed by AV, 18-Feb-2021.) (Revised by AV, 29-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (EulerPathsβπΊ) = {β¨π, πβ© β£ (π(TrailsβπΊ)π β§ π:(0..^(β―βπ))βontoβdom πΌ)} | ||
Theorem | iseupth 28931 | The property "β¨πΉ, πβ© is an Eulerian path on the graph πΊ". An Eulerian path is defined as bijection πΉ from the edges to a set 0...(π β 1) and a function π:(0...π)βΆπ into the vertices such that for each 0 β€ π < π, πΉ(π) is an edge from π(π) to π(π + 1). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(EulerPathsβπΊ)π β (πΉ(TrailsβπΊ)π β§ πΉ:(0..^(β―βπΉ))βontoβdom πΌ)) | ||
Theorem | iseupthf1o 28932 | The property "β¨πΉ, πβ© is an Eulerian path on the graph πΊ". An Eulerian path is defined as bijection πΉ from the edges to a set 0...(π β 1) and a function π:(0...π)βΆπ into the vertices such that for each 0 β€ π < π, πΉ(π) is an edge from π(π) to π(π + 1). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(EulerPathsβπΊ)π β (πΉ(WalksβπΊ)π β§ πΉ:(0..^(β―βπΉ))β1-1-ontoβdom πΌ)) | ||
Theorem | eupthi 28933 | Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(EulerPathsβπΊ)π β (πΉ(WalksβπΊ)π β§ πΉ:(0..^(β―βπΉ))β1-1-ontoβdom πΌ)) | ||
Theorem | eupthf1o 28934 | The πΉ function in an Eulerian path is a bijection from a half-open range of nonnegative integers to the set of edges. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(EulerPathsβπΊ)π β πΉ:(0..^(β―βπΉ))β1-1-ontoβdom πΌ) | ||
Theorem | eupthfi 28935 | Any graph with an Eulerian path is of finite size, i.e. with a finite number of edges. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 18-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ (πΉ(EulerPathsβπΊ)π β dom πΌ β Fin) | ||
Theorem | eupthseg 28936 | The π-th edge in an eulerian path is the edge having π(π) and π(π + 1) as endpoints . (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΉ(EulerPathsβπΊ)π β§ π β (0..^(β―βπΉ))) β {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) | ||
Theorem | upgriseupth 28937* | The property "β¨πΉ, πβ© is an Eulerian path on the pseudograph πΊ". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π = (VtxβπΊ) β β’ (πΊ β UPGraph β (πΉ(EulerPathsβπΊ)π β (πΉ:(0..^(β―βπΉ))β1-1-ontoβdom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | upgreupthi 28938* | Properties of an Eulerian path in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ πΌ = (iEdgβπΊ) & β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(EulerPathsβπΊ)π) β (πΉ:(0..^(β―βπΉ))β1-1-ontoβdom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) | ||
Theorem | upgreupthseg 28939 | The π-th edge in an eulerian path is the edge from π(π) to π(π + 1). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(EulerPathsβπΊ)π β§ π β (0..^(β―βπΉ))) β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) | ||
Theorem | eupthcl 28940 | An Eulerian path has length β―(πΉ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ (πΉ(EulerPathsβπΊ)π β (β―βπΉ) β β0) | ||
Theorem | eupthistrl 28941 | An Eulerian path is a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017.) (Revised by AV, 18-Feb-2021.) |
β’ (πΉ(EulerPathsβπΊ)π β πΉ(TrailsβπΊ)π) | ||
Theorem | eupthiswlk 28942 | An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021.) |
β’ (πΉ(EulerPathsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | eupthpf 28943 | The π function in an Eulerian path is a function from a finite sequence of nonnegative integers to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
β’ (πΉ(EulerPathsβπΊ)π β π:(0...(β―βπΉ))βΆ(VtxβπΊ)) | ||
Theorem | eupth0 28944 | There is an Eulerian path on an empty graph, i.e. a graph with at least one vertex, but without an edge. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 5-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((π΄ β π β§ πΌ = β ) β β (EulerPathsβπΊ){β¨0, π΄β©}) | ||
Theorem | eupthres 28945 | The restriction β¨π», πβ© of an Eulerian path β¨πΉ, πβ© to an initial segment of the path (of length π) forms an Eulerian path on the subgraph π consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(EulerPathsβπΊ)π) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ π» = (πΉ prefix π) & β’ π = (π βΎ (0...π)) & β’ (Vtxβπ) = π β β’ (π β π»(EulerPathsβπ)π) | ||
Theorem | eupthp1 28946 | Append one path segment to an Eulerian path β¨πΉ, πβ© to become an Eulerian path β¨π», πβ© of the supergraph π obtained by adding the new edge to the graph πΊ. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 7-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) (Revised by AV, 8-Apr-2024.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(EulerPathsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©}) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) & β’ π = (π βͺ {β¨(π + 1), πΆβ©}) & β’ (Vtxβπ) = π & β’ ((π β§ πΆ = (πβπ)) β πΈ = {πΆ}) β β’ (π β π»(EulerPathsβπ)π) | ||
Theorem | eupth2eucrct 28947 | Append one path segment to an Eulerian path β¨πΉ, πβ© which may not be an (Eulerian) circuit to become an Eulerian circuit β¨π», πβ© of the supergraph π obtained by adding the new edge to the graph πΊ. (Contributed by AV, 11-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) (Revised by AV, 8-Apr-2024.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β πΌ β Fin) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β Β¬ π΅ β dom πΌ) & β’ (π β πΉ(EulerPathsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β πΈ β (EdgβπΊ)) & β’ (π β {(πβπ), πΆ} β πΈ) & β’ (iEdgβπ) = (πΌ βͺ {β¨π΅, πΈβ©}) & β’ π» = (πΉ βͺ {β¨π, π΅β©}) & β’ π = (π βͺ {β¨(π + 1), πΆβ©}) & β’ (Vtxβπ) = π & β’ ((π β§ πΆ = (πβπ)) β πΈ = {πΆ}) & β’ (π β πΆ = (πβ0)) β β’ (π β (π»(EulerPathsβπ)π β§ π»(Circuitsβπ)π)) | ||
Theorem | eupth2lem1 28948 | Lemma for eupth2 28969. (Contributed by Mario Carneiro, 8-Apr-2015.) |
β’ (π β π β (π β if(π΄ = π΅, β , {π΄, π΅}) β (π΄ β π΅ β§ (π = π΄ β¨ π = π΅)))) | ||
Theorem | eupth2lem2 28949 | Lemma for eupth2 28969. (Contributed by Mario Carneiro, 8-Apr-2015.) |
β’ π΅ β V β β’ ((π΅ β πΆ β§ π΅ = π) β (Β¬ π β if(π΄ = π΅, β , {π΄, π΅}) β π β if(π΄ = πΆ, β , {π΄, πΆ}))) | ||
Theorem | trlsegvdeglem1 28950 | Lemma for trlsegvdeg 28957. (Contributed by AV, 20-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) β β’ (π β ((πβπ) β π β§ (πβ(π + 1)) β π)) | ||
Theorem | trlsegvdeglem2 28951 | Lemma for trlsegvdeg 28957. (Contributed by AV, 20-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β Fun (iEdgβπ)) | ||
Theorem | trlsegvdeglem3 28952 | Lemma for trlsegvdeg 28957. (Contributed by AV, 20-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β Fun (iEdgβπ)) | ||
Theorem | trlsegvdeglem4 28953 | Lemma for trlsegvdeg 28957. (Contributed by AV, 21-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β dom (iEdgβπ) = ((πΉ β (0..^π)) β© dom πΌ)) | ||
Theorem | trlsegvdeglem5 28954 | Lemma for trlsegvdeg 28957. (Contributed by AV, 21-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β dom (iEdgβπ) = {(πΉβπ)}) | ||
Theorem | trlsegvdeglem6 28955 | Lemma for trlsegvdeg 28957. (Contributed by AV, 21-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β dom (iEdgβπ) β Fin) | ||
Theorem | trlsegvdeglem7 28956 | Lemma for trlsegvdeg 28957. (Contributed by AV, 21-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β dom (iEdgβπ) β Fin) | ||
Theorem | trlsegvdeg 28957 | Formerly part of proof of eupth2lem3 28966: If a trail in a graph πΊ induces a subgraph π with the vertices π of πΊ and the edges being the edges of the walk, and a subgraph π with the vertices π of πΊ and the edges being the edges of the walk except the last one, and a subgraph π with the vertices π of πΊ and one edges being the last edge of the walk, then the vertex degree of any vertex π of πΊ within π is the sum of the vertex degree of π within π and the vertex degree of π within π. Note that this theorem would not hold for arbitrary walks (if the last edge was identical with a previous edge, the degree of the vertices incident with this edge would not be increased because of this edge). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β ((VtxDegβπ)βπ) = (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ))) | ||
Theorem | eupth2lem3lem1 28958 | Lemma for eupth2lem3 28966. (Contributed by AV, 21-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β ((VtxDegβπ)βπ) β β0) | ||
Theorem | eupth2lem3lem2 28959 | Lemma for eupth2lem3 28966. (Contributed by AV, 21-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) β β’ (π β ((VtxDegβπ)βπ) β β0) | ||
Theorem | eupth2lem3lem3 28960* | Lemma for eupth2lem3 28966, formerly part of proof of eupth2lem3 28966: If a loop {(πβπ), (πβ(π + 1))} is added to a trail, the degree of the vertices with odd degree remains odd (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 21-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) & β’ (π β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β , {(πβ0), (πβπ)})) & β’ (π β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) β β’ ((π β§ (πβπ) = (πβ(π + 1))) β (Β¬ 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β , {(πβ0), (πβ(π + 1))}))) | ||
Theorem | eupth2lem3lem4 28961* | Lemma for eupth2lem3 28966, formerly part of proof of eupth2lem3 28966: If an edge (not a loop) is added to a trail, the degree of the end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) & β’ (π β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β , {(πβ0), (πβπ)})) & β’ (π β if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) & β’ (π β (πΌβ(πΉβπ)) β π« π) β β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π = (πβπ) β¨ π = (πβ(π + 1)))) β (Β¬ 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β , {(πβ0), (πβ(π + 1))}))) | ||
Theorem | eupth2lem3lem5 28962* | Lemma for eupth2 28969. (Contributed by AV, 25-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) & β’ (π β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β , {(πβ0), (πβπ)})) & β’ (π β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β β’ (π β (πΌβ(πΉβπ)) β π« π) | ||
Theorem | eupth2lem3lem6 28963* | Formerly part of proof of eupth2lem3 28966: If an edge (not a loop) is added to a trail, the degree of vertices not being end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). Remark: This seems to be not valid for hyperedges joining more vertices than (πβ0) and (πβπ): if there is a third vertex in the edge, and this vertex is already contained in the trail, then the degree of this vertex could be affected by this edge! (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) & β’ (π β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β , {(πβ0), (πβπ)})) & β’ (π β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β β’ ((π β§ (πβπ) β (πβ(π + 1)) β§ (π β (πβπ) β§ π β (πβ(π + 1)))) β (Β¬ 2 β₯ (((VtxDegβπ)βπ) + ((VtxDegβπ)βπ)) β π β if((πβ0) = (πβ(π + 1)), β , {(πβ0), (πβ(π + 1))}))) | ||
Theorem | eupth2lem3lem7 28964* | Lemma for eupth2lem3 28966: Combining trlsegvdeg 28957, eupth2lem3lem3 28960, eupth2lem3lem4 28961 and eupth2lem3lem6 28963. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 27-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β Fun πΌ) & β’ (π β π β (0..^(β―βπΉ))) & β’ (π β π β π) & β’ (π β πΉ(TrailsβπΊ)π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (Vtxβπ) = π) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ (π β (iEdgβπ) = {β¨(πΉβπ), (πΌβ(πΉβπ))β©}) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0...π)))) & β’ (π β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπ)βπ₯)} = if((πβ0) = (πβπ), β , {(πβ0), (πβπ)})) & β’ (π β (πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}) β β’ (π β (Β¬ 2 β₯ ((VtxDegβπ)βπ) β π β if((πβ0) = (πβ(π + 1)), β , {(πβ0), (πβ(π + 1))}))) | ||
Theorem | eupthvdres 28965 | Formerly part of proof of eupth2 28969: The vertex degree remains the same for all vertices if the edges are restricted to the edges of an Eulerian path. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΊ β π) & β’ (π β Fun πΌ) & β’ (π β πΉ(EulerPathsβπΊ)π) & β’ π» = β¨π, (πΌ βΎ (πΉ β (0..^(β―βπΉ))))β© β β’ (π β (VtxDegβπ») = (VtxDegβπΊ)) | ||
Theorem | eupth2lem3 28966* | Lemma for eupth2 28969. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΊ β UPGraph) & β’ (π β Fun πΌ) & β’ (π β πΉ(EulerPathsβπΊ)π) & β’ π» = β¨π, (πΌ βΎ (πΉ β (0..^π)))β© & β’ π = β¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β© & β’ (π β π β β0) & β’ (π β (π + 1) β€ (β―βπΉ)) & β’ (π β π β π) & β’ (π β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπ»)βπ₯)} = if((πβ0) = (πβπ), β , {(πβ0), (πβπ)})) β β’ (π β (Β¬ 2 β₯ ((VtxDegβπ)βπ) β π β if((πβ0) = (πβ(π + 1)), β , {(πβ0), (πβ(π + 1))}))) | ||
Theorem | eupth2lemb 28967* | Lemma for eupth2 28969 (induction basis): There are no vertices of odd degree in an Eulerian path of length 0, having no edge and identical endpoints (the single vertex of the Eulerian path). Formerly part of proof for eupth2 28969. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΊ β UPGraph) & β’ (π β Fun πΌ) & β’ (π β πΉ(EulerPathsβπΊ)π) β β’ (π β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^0)))β©)βπ₯)} = β ) | ||
Theorem | eupth2lems 28968* | Lemma for eupth2 28969 (induction step): The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct, if the Eulerian path shortened by one edge has this property. Formerly part of proof for eupth2 28969. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΊ β UPGraph) & β’ (π β Fun πΌ) & β’ (π β πΉ(EulerPathsβπΊ)π) β β’ ((π β§ π β β0) β ((π β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^π)))β©)βπ₯)} = if((πβ0) = (πβπ), β , {(πβ0), (πβπ)})) β ((π + 1) β€ (β―βπΉ) β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegββ¨π, (πΌ βΎ (πΉ β (0..^(π + 1))))β©)βπ₯)} = if((πβ0) = (πβ(π + 1)), β , {(πβ0), (πβ(π + 1))})))) | ||
Theorem | eupth2 28969* | The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΊ β UPGraph) & β’ (π β Fun πΌ) & β’ (π β πΉ(EulerPathsβπΊ)π) β β’ (π β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπΊ)βπ₯)} = if((πβ0) = (πβ(β―βπΉ)), β , {(πβ0), (πβ(β―βπΉ))})) | ||
Theorem | eulerpathpr 28970* | A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(EulerPathsβπΊ)π) β (β―β{π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπΊ)βπ₯)}) β {0, 2}) | ||
Theorem | eulerpath 28971* | A pseudograph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ (EulerPathsβπΊ) β β ) β (β―β{π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπΊ)βπ₯)}) β {0, 2}) | ||
Theorem | eulercrct 28972* | A pseudograph with an Eulerian circuit β¨πΉ, πβ© (an "Eulerian pseudograph") has only vertices of even degree. (Contributed by AV, 12-Mar-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β UPGraph β§ πΉ(EulerPathsβπΊ)π β§ πΉ(CircuitsβπΊ)π) β βπ₯ β π 2 β₯ ((VtxDegβπΊ)βπ₯)) | ||
Theorem | eucrctshift 28973* | Cyclically shifting the indices of an Eulerian circuit β¨πΉ, πβ© results in an Eulerian circuit β¨π», πβ©. (Contributed by AV, 15-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ (π β πΉ(EulerPathsβπΊ)π) β β’ (π β (π»(EulerPathsβπΊ)π β§ π»(CircuitsβπΊ)π)) | ||
Theorem | eucrct2eupth1 28974 | Removing one edge (πΌβ(πΉβπ)) from a nonempty graph πΊ with an Eulerian circuit β¨πΉ, πβ© results in a graph π with an Eulerian path β¨π», πβ©. This is the special case of eucrct2eupth 28975 (with π½ = (π β 1)) where the last segment/edge of the circuit is removed. (Contributed by AV, 11-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(EulerPathsβπΊ)π) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ (Vtxβπ) = π & β’ (π β 0 < (β―βπΉ)) & β’ (π β π = ((β―βπΉ) β 1)) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β (0..^π)))) & β’ π» = (πΉ prefix π) & β’ π = (π βΎ (0...π)) β β’ (π β π»(EulerPathsβπ)π) | ||
Theorem | eucrct2eupth 28975* | Removing one edge (πΌβ(πΉβπ½)) from a graph πΊ with an Eulerian circuit β¨πΉ, πβ© results in a graph π with an Eulerian path β¨π», πβ©. (Contributed by AV, 17-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(EulerPathsβπΊ)π) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ (Vtxβπ) = π & β’ (π β π = (β―βπΉ)) & β’ (π β π½ β (0..^π)) & β’ (π β (iEdgβπ) = (πΌ βΎ (πΉ β ((0..^π) β {π½})))) & β’ πΎ = (π½ + 1) & β’ π» = ((πΉ cyclShift πΎ) prefix (π β 1)) & β’ π = (π₯ β (0..^π) β¦ if(π₯ β€ (π β πΎ), (πβ(π₯ + πΎ)), (πβ((π₯ + πΎ) β π)))) β β’ (π β π»(EulerPathsβπ)π) | ||
According to Wikipedia ("Seven Bridges of KΓΆnigsberg", 9-Mar-2021, https://en.wikipedia.org/wiki/Seven_Bridges_of_Koenigsberg): "The Seven Bridges of KΓΆnigsberg is a historically notable problem in mathematics. Its negative resolution by Leonhard Euler in 1736 laid the foundations of graph theory and prefigured the idea of topology. The city of KΓΆnigsberg in [East] Prussia (now Kaliningrad, Russia) was set on both sides of the Pregel River, and included two large islands - Kneiphof and Lomse - which were connected to each other, or to the two mainland portions of the city, by seven bridges. The problem was to devise a walk through the city that would cross each of those bridges once and only once.". Euler proved that the problem has no solution by applying Euler's theorem to the KΓΆnigsberg graph, which is obtained by replacing each land mass with an abstract "vertex" or node, and each bridge with an abstract connection, an "edge", which connects two land masses/vertices. The KΓΆnigsberg graph πΊ is a multigraph consisting of 4 vertices and 7 edges, represented by the following ordered pair: πΊ = β¨(0...3), β¨β{0, 1}{0, 2} {0, 3}{1, 2}{1, 2}{2, 3}{2, 3}ββ©β©, see konigsbergumgr 28981. konigsberg 28987 shows that the KΓΆnigsberg graph has no Eulerian path, thus the KΓΆnigsberg Bridge problem has no solution. | ||
Theorem | konigsbergvtx 28976 | The set of vertices of the KΓΆnigsberg graph πΊ. (Contributed by AV, 28-Feb-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ (VtxβπΊ) = (0...3) | ||
Theorem | konigsbergiedg 28977 | The indexed edges of the KΓΆnigsberg graph πΊ. (Contributed by AV, 28-Feb-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ (iEdgβπΊ) = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© | ||
Theorem | konigsbergiedgw 28978* | The indexed edges of the KΓΆnigsberg graph πΊ is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ πΈ β Word {π₯ β π« π β£ (β―βπ₯) = 2} | ||
Theorem | konigsbergssiedgwpr 28979* | Each subset of the indexed edges of the KΓΆnigsberg graph πΊ is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ ((π΄ β Word V β§ π΅ β Word V β§ πΈ = (π΄ ++ π΅)) β π΄ β Word {π₯ β π« π β£ (β―βπ₯) = 2}) | ||
Theorem | konigsbergssiedgw 28980* | Each subset of the indexed edges of the KΓΆnigsberg graph πΊ is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ ((π΄ β Word V β§ π΅ β Word V β§ πΈ = (π΄ ++ π΅)) β π΄ β Word {π₯ β (π« π β {β }) β£ (β―βπ₯) β€ 2}) | ||
Theorem | konigsbergumgr 28981 | The KΓΆnigsberg graph πΊ is a multigraph. (Contributed by AV, 28-Feb-2021.) (Revised by AV, 9-Mar-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ πΊ β UMGraph | ||
Theorem | konigsberglem1 28982 | Lemma 1 for konigsberg 28987: Vertex 0 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ ((VtxDegβπΊ)β0) = 3 | ||
Theorem | konigsberglem2 28983 | Lemma 2 for konigsberg 28987: Vertex 1 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ ((VtxDegβπΊ)β1) = 3 | ||
Theorem | konigsberglem3 28984 | Lemma 3 for konigsberg 28987: Vertex 3 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ ((VtxDegβπΊ)β3) = 3 | ||
Theorem | konigsberglem4 28985* | Lemma 4 for konigsberg 28987: Vertices 0, 1, 3 are vertices of odd degree. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ {0, 1, 3} β {π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπΊ)βπ₯)} | ||
Theorem | konigsberglem5 28986* | Lemma 5 for konigsberg 28987: The set of vertices of odd degree is greater than 2. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ 2 < (β―β{π₯ β π β£ Β¬ 2 β₯ ((VtxDegβπΊ)βπ₯)}) | ||
Theorem | konigsberg 28987 | The KΓΆnigsberg Bridge problem. If πΊ is the KΓΆnigsberg graph, i.e. a graph on four vertices 0, 1, 2, 3, with edges {0, 1}, {0, 2}, {0, 3}, {1, 2}, {1, 2}, {2, 3}, {2, 3}, then vertices 0, 1, 3 each have degree three, and 2 has degree five, so there are four vertices of odd degree and thus by eulerpath 28971 the graph cannot have an Eulerian path. It is sufficient to show that there are 3 vertices of odd degree, since a graph having an Eulerian path can only have 0 or 2 vertices of odd degree. This is Metamath 100 proof #54. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 9-Mar-2021.) |
β’ π = (0...3) & β’ πΈ = β¨β{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}ββ© & β’ πΊ = β¨π, πΈβ© β β’ (EulerPathsβπΊ) = β | ||
Syntax | cfrgr 28988 | Extend class notation with friendship graphs. |
class FriendGraph | ||
Definition | df-frgr 28989* | Define the class of all friendship graphs: a simple graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. This condition is called the friendship condition , see definition in [MertziosUnger] p. 152. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.) (Revised by AV, 29-Mar-2021.) (Revised by AV, 3-Jan-2024.) |
β’ FriendGraph = {π β USGraph β£ [(Vtxβπ) / π£][(Edgβπ) / π]βπ β π£ βπ β (π£ β {π})β!π₯ β π£ {{π₯, π}, {π₯, π}} β π} | ||
Theorem | isfrgr 28990* | The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) (Revised by AV, 3-Jan-2024.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β (πΊ β USGraph β§ βπ β π βπ β (π β {π})β!π₯ β π {{π₯, π}, {π₯, π}} β πΈ)) | ||
Theorem | frgrusgr 28991 | A friendship graph is a simple graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
β’ (πΊ β FriendGraph β πΊ β USGraph) | ||
Theorem | frgr0v 28992 | Any null graph (set with no vertices) is a friendship graph iff its edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β ) β (πΊ β FriendGraph β (iEdgβπΊ) = β )) | ||
Theorem | frgr0vb 28993 | Any null graph (without vertices and edges) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 29-Mar-2021.) |
β’ ((πΊ β π β§ (VtxβπΊ) = β β§ (iEdgβπΊ) = β ) β πΊ β FriendGraph ) | ||
Theorem | frgruhgr0v 28994 | Any null graph (without vertices) represented as hypergraph is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
β’ ((πΊ β UHGraph β§ (VtxβπΊ) = β ) β πΊ β FriendGraph ) | ||
Theorem | frgr0 28995 | The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
β’ β β FriendGraph | ||
Theorem | frcond1 28996* | The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β ((π΄ β π β§ πΆ β π β§ π΄ β πΆ) β β!π β π {{π΄, π}, {π, πΆ}} β πΈ)) | ||
Theorem | frcond2 28997* | The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β ((π΄ β π β§ πΆ β π β§ π΄ β πΆ) β β!π β π ({π΄, π} β πΈ β§ {π, πΆ} β πΈ))) | ||
Theorem | frgreu 28998* | Variant of frcond2 28997: Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 4-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β ((π΄ β π β§ πΆ β π β§ π΄ β πΆ) β β!π({π΄, π} β πΈ β§ {π, πΆ} β πΈ))) | ||
Theorem | frcond3 28999* | The friendship condition, expressed by neighborhoods: in a friendship graph, the neighborhood of a vertex and the neighborhood of a second, different vertex have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 30-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β ((π΄ β π β§ πΆ β π β§ π΄ β πΆ) β βπ₯ β π ((πΊ NeighbVtx π΄) β© (πΊ NeighbVtx πΆ)) = {π₯})) | ||
Theorem | frcond4 29000* | The friendship condition, alternatively expressed by neighborhoods: in a friendship graph, the neighborhoods of two different vertices have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.) (Proof shortened by AV, 30-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β βπ β π βπ β (π β {π})βπ₯ β π ((πΊ NeighbVtx π) β© (πΊ NeighbVtx π)) = {π₯}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |