![]() |
Metamath
Proof Explorer Theorem List (p. 299 of 480) | < 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: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1to3vfriendship 29801* | The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((π΄ β π β§ (π = {π΄} β¨ π = {π΄, π΅} β¨ π = {π΄, π΅, πΆ})) β (πΊ β FriendGraph β βπ£ β π βπ€ β (π β {π£}){π£, π€} β πΈ)) | ||
Theorem | 2pthfrgrrn 29802* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 15-Nov-2017.) (Revised by AV, 1-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β βπ β π βπ β (π β {π})βπ β π ({π, π} β πΈ β§ {π, π} β πΈ)) | ||
Theorem | 2pthfrgrrn2 29803* | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 16-Nov-2017.) (Revised by AV, 1-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β βπ β π βπ β (π β {π})βπ β π (({π, π} β πΈ β§ {π, π} β πΈ) β§ (π β π β§ π β π))) | ||
Theorem | 2pthfrgr 29804* | Between any two (different) vertices in a friendship graph, tere is a 2-path (simple path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 1-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (πΊ β FriendGraph β βπ β π βπ β (π β {π})βπβπ(π(π(SPathsOnβπΊ)π)π β§ (β―βπ) = 2)) | ||
Theorem | 3cyclfrgrrn1 29805* | Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ (π΄ β π β§ πΆ β π) β§ π΄ β πΆ) β βπ β π βπ β π ({π΄, π} β πΈ β§ {π, π} β πΈ β§ {π, π΄} β πΈ)) | ||
Theorem | 3cyclfrgrrn 29806* | Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ 1 < (β―βπ)) β βπ β π βπ β π βπ β π ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ)) | ||
Theorem | 3cyclfrgrrn2 29807* | Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 2-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ 1 < (β―βπ)) β βπ β π βπ β π βπ β π (π β π β§ ({π, π} β πΈ β§ {π, π} β πΈ β§ {π, π} β πΈ))) | ||
Theorem | 3cyclfrgr 29808* | Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ 1 < (β―βπ)) β βπ£ β π βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π£)) | ||
Theorem | 4cycl2v2nb 29809 | In a (maybe degenerate) 4-cycle, two vertice have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
β’ ((({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({πΆ, π·} β πΈ β§ {π·, π΄} β πΈ)) β ({{π΄, π΅}, {π΅, πΆ}} β πΈ β§ {{π΄, π·}, {π·, πΆ}} β πΈ)) | ||
Theorem | 4cycl2vnunb 29810* | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
β’ ((({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({πΆ, π·} β πΈ β§ {π·, π΄} β πΈ) β§ (π΅ β π β§ π· β π β§ π΅ β π·)) β Β¬ β!π₯ β π {{π΄, π₯}, {π₯, πΆ}} β πΈ) | ||
Theorem | n4cyclfrgr 29811 | There is no 4-cycle in a friendship graph, see Proposition 1(a) of [MertziosUnger] p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.) |
β’ ((πΊ β FriendGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 4) | ||
Theorem | 4cyclusnfrgr 29812 | A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 2-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β USGraph β§ (π΄ β π β§ πΆ β π β§ π΄ β πΆ) β§ (π΅ β π β§ π· β π β§ π΅ β π·)) β ((({π΄, π΅} β πΈ β§ {π΅, πΆ} β πΈ) β§ ({πΆ, π·} β πΈ β§ {π·, π΄} β πΈ)) β πΊ β FriendGraph )) | ||
Theorem | frgrnbnb 29813 | If two neighbors π and π of a vertex π have a common neighbor π΄ in a friendship graph, then this common neighbor π΄ must be the vertex π. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 2-Apr-2021.) (Proof shortened by AV, 13-Feb-2022.) |
β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) β β’ ((πΊ β FriendGraph β§ (π β π· β§ π β π·) β§ π β π) β (({π, π΄} β πΈ β§ {π, π΄} β πΈ) β π΄ = π)) | ||
Theorem | frgrconngr 29814 | A friendship graph is connected, see remark 1 in [MertziosUnger] p. 153 (after Proposition 1): "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 1-Apr-2021.) |
β’ (πΊ β FriendGraph β πΊ β ConnGraph) | ||
Theorem | vdgn0frgrv2 29815 | A vertex in a friendship graph 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βπΊ) β β’ ((πΊ β FriendGraph β§ π β π) β (1 < (β―βπ) β ((VtxDegβπΊ)βπ) β 0)) | ||
Theorem | vdgn1frgrv2 29816 | Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ π β π) β (1 < (β―βπ) β ((VtxDegβπΊ)βπ) β 1)) | ||
Theorem | vdgn1frgrv3 29817* | Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 4-Sep-2018.) (Revised by AV, 4-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ 1 < (β―βπ)) β βπ£ β π ((VtxDegβπΊ)βπ£) β 1) | ||
Theorem | vdgfrgrgt2 29818 | Any vertex in a friendship graph (with more than one vertex - then, actually, the graph must have at least three vertices, because otherwise, it would not be a friendship graph) has at least degree 2, see remark 3 in [MertziosUnger] p. 153 (after Proposition 1): "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 5-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ π β π) β (1 < (β―βπ) β 2 β€ ((VtxDegβπΊ)βπ))) | ||
In this section, the friendship theorem friendship 29919 is proven by formalizing Huneke's proof, see [Huneke] pp. 1-2. The three claims (see frgrncvvdeq 29829, frgrregorufr 29845 and frrusgrord0 29860) and additional statements (numbered in the order of their occurrence in the paper) in Huneke's proof are cited in the corresponding theorems. | ||
Theorem | frgrncvvdeqlem1 29819 | Lemma 1 for frgrncvvdeq 29829. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 8-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ (π β π β π) | ||
Theorem | frgrncvvdeqlem2 29820* | Lemma 2 for frgrncvvdeq 29829. In a friendship graph, for each neighbor of a vertex there is exactly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ ((π β§ π₯ β π·) β β!π¦ β π {π₯, π¦} β πΈ) | ||
Theorem | frgrncvvdeqlem3 29821* | Lemma 3 for frgrncvvdeq 29829. The unique neighbor of a vertex (expressed by a restricted iota) is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ ((π β§ π₯ β π·) β {(β©π¦ β π {π₯, π¦} β πΈ)} = ((πΊ NeighbVtx π₯) β© π)) | ||
Theorem | frgrncvvdeqlem4 29822* | Lemma 4 for frgrncvvdeq 29829. The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 10-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ (π β π΄:π·βΆπ) | ||
Theorem | frgrncvvdeqlem5 29823* | Lemma 5 for frgrncvvdeq 29829. The mapping of neighbors to neighbors applied on a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ ((π β§ π₯ β π·) β {(π΄βπ₯)} = ((πΊ NeighbVtx π₯) β© π)) | ||
Theorem | frgrncvvdeqlem6 29824* | Lemma 6 for frgrncvvdeq 29829. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ ((π β§ π₯ β π·) β {π₯, (π΄βπ₯)} β πΈ) | ||
Theorem | frgrncvvdeqlem7 29825* | Lemma 7 for frgrncvvdeq 29829. This corresponds to statement 1 in [Huneke] p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ (π β βπ₯ β π· (π΄βπ₯) β π) | ||
Theorem | frgrncvvdeqlem8 29826* | Lemma 8 for frgrncvvdeq 29829. This corresponds to statement 2 in [Huneke] p. 1: "The map is one-to-one since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) (Revised by AV, 30-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ (π β π΄:π·β1-1βπ) | ||
Theorem | frgrncvvdeqlem9 29827* | Lemma 9 for frgrncvvdeq 29829. This corresponds to statement 3 in [Huneke] p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ (π β π΄:π·βontoβπ) | ||
Theorem | frgrncvvdeqlem10 29828* | Lemma 10 for frgrncvvdeq 29829. (Contributed by Alexander van der Vekens, 24-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (πΊ NeighbVtx π) & β’ π = (πΊ NeighbVtx π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π·) & β’ (π β πΊ β FriendGraph ) & β’ π΄ = (π₯ β π· β¦ (β©π¦ β π {π₯, π¦} β πΈ)) β β’ (π β π΄:π·β1-1-ontoβπ) | ||
Theorem | frgrncvvdeq 29829* | In a friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to claim 1 in [Huneke] p. 1: "If x,y are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 10-May-2021.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) β β’ (πΊ β FriendGraph β βπ₯ β π βπ¦ β (π β {π₯})(π¦ β (πΊ NeighbVtx π₯) β (π·βπ₯) = (π·βπ¦))) | ||
Theorem | frgrwopreglem4a 29830 | In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 29835 without a fixed degree and without using the sets π΄ and π΅. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 4-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ (π β π β§ π β π) β§ (π·βπ) β (π·βπ)) β {π, π} β πΈ) | ||
Theorem | frgrwopreglem5a 29831 | If a friendship graph has two vertices with the same degree and two other vertices with different degrees, then there is a 4-cycle in the graph. Alternate version of frgrwopreglem5 29841 without a fixed degree and without using the sets π΄ and π΅. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 4-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ ((π΄ β π β§ π β π) β§ (π΅ β π β§ π β π)) β§ ((π·βπ΄) = (π·βπ) β§ (π·βπ΄) β (π·βπ΅) β§ (π·βπ) β (π·βπ))) β (({π΄, π΅} β πΈ β§ {π΅, π} β πΈ) β§ ({π, π} β πΈ β§ {π, π΄} β πΈ))) | ||
Theorem | frgrwopreglem1 29832* | Lemma 1 for frgrwopreg 29843: the classes π΄ and π΅ are sets. The definition of π΄ and π΅ corresponds to definition 3 in [Huneke] p. 2: "Let A be the set of all vertices of degree k, let B be the set of all vertices of degree different from k, ..." (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 10-May-2021.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) β β’ (π΄ β V β§ π΅ β V) | ||
Theorem | frgrwopreglem2 29833* | Lemma 2 for frgrwopreg 29843. If the set π΄ of vertices of degree πΎ is not empty in a friendship graph with at least two vertices, then πΎ must be greater than 1 . This is only an observation, which is not required for the proof the friendship theorem. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 2-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) β β’ ((πΊ β FriendGraph β§ 1 < (β―βπ) β§ π΄ β β ) β 2 β€ πΎ) | ||
Theorem | frgrwopreglem3 29834* | Lemma 3 for frgrwopreg 29843. The vertices in the sets π΄ and π΅ have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 2-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) β β’ ((π β π΄ β§ π β π΅) β (π·βπ) β (π·βπ)) | ||
Theorem | frgrwopreglem4 29835* | Lemma 4 for frgrwopreg 29843. In a friendship graph each vertex with degree πΎ is connected with any vertex with degree other than πΎ. This corresponds to statement 4 in [Huneke] p. 2: "By the first claim, every vertex in A is adjacent to every vertex in B.". (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 4-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β βπ β π΄ βπ β π΅ {π, π} β πΈ) | ||
Theorem | frgrwopregasn 29836* | According to statement 5 in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". This version of frgrwopreg1 29838 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Revised by AV, 4-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ π β π β§ π΄ = {π}) β βπ€ β (π β {π}){π, π€} β πΈ) | ||
Theorem | frgrwopregbsn 29837* | According to statement 5 in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". This version of frgrwopreg2 29839 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by AV, 4-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ π β π β§ π΅ = {π}) β βπ€ β (π β {π}){π, π€} β πΈ) | ||
Theorem | frgrwopreg1 29838* | According to statement 5 in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Proof shortened by AV, 4-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ (β―βπ΄) = 1) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β πΈ) | ||
Theorem | frgrwopreg2 29839* | According to statement 5 in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Proof shortened by AV, 4-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ (β―βπ΅) = 1) β βπ£ β π βπ€ β (π β {π£}){π£, π€} β πΈ) | ||
Theorem | frgrwopreglem5lem 29840* | Lemma for frgrwopreglem5 29841. (Contributed by AV, 5-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) & β’ πΈ = (EdgβπΊ) β β’ (((π β π΄ β§ π₯ β π΄) β§ (π β π΅ β§ π¦ β π΅)) β ((π·βπ) = (π·βπ₯) β§ (π·βπ) β (π·βπ) β§ (π·βπ₯) β (π·βπ¦))) | ||
Theorem | frgrwopreglem5 29841* | Lemma 5 for frgrwopreg 29843. If π΄ as well as π΅ contain at least two vertices, there is a 4-cycle in a friendship graph. This corresponds to statement 6 in [Huneke] p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Proof shortened by AV, 5-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ 1 < (β―βπ΄) β§ 1 < (β―βπ΅)) β βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ))) | ||
Theorem | frgrwopreglem5ALT 29842* | Alternate direct proof of frgrwopreglem5 29841, not using frgrwopreglem5a 29831. This proof would be even a little bit shorter than the proof of frgrwopreglem5 29841 without using frgrwopreglem5lem 29840. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 3-Jan-2022.) (Proof shortened by AV, 5-Feb-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) & β’ πΈ = (EdgβπΊ) β β’ ((πΊ β FriendGraph β§ 1 < (β―βπ΄) β§ 1 < (β―βπ΅)) β βπ β π΄ βπ₯ β π΄ βπ β π΅ βπ¦ β π΅ ((π β π₯ β§ π β π¦) β§ ({π, π} β πΈ β§ {π, π₯} β πΈ) β§ ({π₯, π¦} β πΈ β§ {π¦, π} β πΈ))) | ||
Theorem | frgrwopreg 29843* | In a friendship graph there are either no vertices (π΄ = β ) or exactly one vertex ((β―βπ΄) = 1) having degree πΎ, or all (π΅ = β ) or all except one vertices ((β―βπ΅) = 1) have degree πΎ. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 3-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ π· = (VtxDegβπΊ) & β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} & β’ π΅ = (π β π΄) β β’ (πΊ β FriendGraph β (((β―βπ΄) = 1 β¨ π΄ = β ) β¨ ((β―βπ΅) = 1 β¨ π΅ = β ))) | ||
Theorem | frgrregorufr0 29844* | In a friendship graph there are either no vertices having degree πΎ, or all vertices have degree πΎ for any (nonnegative integer) πΎ, unless there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Revised by AV, 11-May-2021.) (Proof shortened by AV, 3-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ (πΊ β FriendGraph β (βπ£ β π (π·βπ£) = πΎ β¨ βπ£ β π (π·βπ£) β πΎ β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β πΈ)) | ||
Theorem | frgrregorufr 29845* | If there is a vertex having degree πΎ for each (nonnegative integer) πΎ in a friendship graph, then either all vertices have degree πΎ or there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π· = (VtxDegβπΊ) β β’ (πΊ β FriendGraph β (βπ β π (π·βπ) = πΎ β (βπ£ β π (π·βπ£) = πΎ β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β πΈ))) | ||
Theorem | frgrregorufrg 29846* | If there is a vertex having degree π for each nonnegative integer π in a friendship graph, then there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". Variant of frgrregorufr 29845 with generalization. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Revised by AV, 26-May-2021.) (Proof shortened by AV, 12-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (πΊ β FriendGraph β βπ β β0 (βπ β π ((VtxDegβπΊ)βπ) = π β (πΊ RegUSGraph π β¨ βπ£ β π βπ€ β (π β {π£}){π£, π€} β πΈ))) | ||
Theorem | frgr2wwlkeu 29847* | For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 4-Jan-2022.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ (π΄ β π β§ π΅ β π) β§ π΄ β π΅) β β!π β π β¨βπ΄ππ΅ββ© β (π΄(2 WWalksNOn πΊ)π΅)) | ||
Theorem | frgr2wwlkn0 29848 | In a friendship graph, there is always a path/walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ (π΄ β π β§ π΅ β π) β§ π΄ β π΅) β (π΄(2 WWalksNOn πΊ)π΅) β β ) | ||
Theorem | frgr2wwlk1 29849 | In a friendship graph, there is exactly one walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) (Revised by AV, 13-May-2021.) (Proof shortened by AV, 16-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ (π΄ β π β§ π΅ β π) β§ π΄ β π΅) β (β―β(π΄(2 WWalksNOn πΊ)π΅)) = 1) | ||
Theorem | frgr2wsp1 29850 | In a friendship graph, there is exactly one simple path of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 13-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ (π΄ β π β§ π΅ β π) β§ π΄ β π΅) β (β―β(π΄(2 WSPathsNOn πΊ)π΅)) = 1) | ||
Theorem | frgr2wwlkeqm 29851 | If there is a (simple) path of length 2 from one vertex to another vertex and a (simple) path of length 2 from the other vertex back to the first vertex in a friendship graph, then the middle vertex is the same. This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 20-Feb-2018.) (Revised by AV, 13-May-2021.) (Proof shortened by AV, 7-Jan-2022.) |
β’ ((πΊ β FriendGraph β§ π΄ β π΅ β§ (π β π β§ π β π)) β ((β¨βπ΄ππ΅ββ© β (π΄(2 WWalksNOn πΊ)π΅) β§ β¨βπ΅ππ΄ββ© β (π΅(2 WWalksNOn πΊ)π΄)) β π = π)) | ||
Theorem | frgrhash2wsp 29852 | The number of simple paths of length 2 is n*(n-1) in a friendship graph with n vertices. This corresponds to the proof of claim 3 in [Huneke] p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, Huneke counts undirected paths, so obtains the result ((πC2) = ((π Β· (π β 1)) / 2)), whereas we count directed paths, obtaining twice that number. (Contributed by Alexander van der Vekens, 6-Mar-2018.) (Revised by AV, 10-Jan-2022.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ π β Fin) β (β―β(2 WSPathsN πΊ)) = ((β―βπ) Β· ((β―βπ) β 1))) | ||
Theorem | fusgreg2wsplem 29853* | Lemma for fusgreg2wsp 29856 and related theorems. (Contributed by AV, 8-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π β π β¦ {π€ β (2 WSPathsN πΊ) β£ (π€β1) = π}) β β’ (π β π β (π β (πβπ) β (π β (2 WSPathsN πΊ) β§ (πβ1) = π))) | ||
Theorem | fusgr2wsp2nb 29854* | The set of paths of length 2 with a given vertex in the middle for a finite simple graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 16-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π β π β¦ {π€ β (2 WSPathsN πΊ) β£ (π€β1) = π}) β β’ ((πΊ β FinUSGraph β§ π β π) β (πβπ) = βͺ π₯ β (πΊ NeighbVtx π)βͺ π¦ β ((πΊ NeighbVtx π) β {π₯}){β¨βπ₯ππ¦ββ©}) | ||
Theorem | fusgreghash2wspv 29855* | According to statement 7 in [Huneke] p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For directed simple paths of length 2 represented by length 3 strings, we have again k*(k-1) such paths, see also comment of frgrhash2wsp 29852. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 12-Feb-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π β π β¦ {π€ β (2 WSPathsN πΊ) β£ (π€β1) = π}) β β’ (πΊ β FinUSGraph β βπ£ β π (((VtxDegβπΊ)βπ£) = πΎ β (β―β(πβπ£)) = (πΎ Β· (πΎ β 1)))) | ||
Theorem | fusgreg2wsp 29856* | In a finite simple graph, the set of all paths of length 2 is the union of all the paths of length 2 over the vertices which are in the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 10-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π β π β¦ {π€ β (2 WSPathsN πΊ) β£ (π€β1) = π}) β β’ (πΊ β FinUSGraph β (2 WSPathsN πΊ) = βͺ π₯ β π (πβπ₯)) | ||
Theorem | 2wspmdisj 29857* | The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 10-Jan-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π β π β¦ {π€ β (2 WSPathsN πΊ) β£ (π€β1) = π}) β β’ Disj π₯ β π (πβπ₯) | ||
Theorem | fusgreghash2wsp 29858* | In a finite k-regular graph with N vertices there are N times "k choose 2" paths with length 2, according to statement 8 in [Huneke] p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by length 3 strings, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 19-May-2021.) (Proof shortened by AV, 12-Jan-2022.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FinUSGraph β§ π β β ) β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (β―β(2 WSPathsN πΊ)) = ((β―βπ) Β· (πΎ Β· (πΎ β 1))))) | ||
Theorem | frrusgrord0lem 29859* | Lemma for frrusgrord0 29860. (Contributed by AV, 12-Jan-2022.) |
β’ π = (VtxβπΊ) β β’ (((πΊ β FriendGraph β§ π β Fin β§ π β β ) β§ βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (πΎ β β β§ (β―βπ) β β β§ (β―βπ) β 0)) | ||
Theorem | frrusgrord0 29860* | If a nonempty finite friendship graph is k-regular, its order is k(k-1)+1. This corresponds to claim 3 in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 26-May-2021.) (Proof shortened by AV, 12-Jan-2022.) |
β’ π = (VtxβπΊ) β β’ ((πΊ β FriendGraph β§ π β Fin β§ π β β ) β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (β―βπ) = ((πΎ Β· (πΎ β 1)) + 1))) | ||
Theorem | frrusgrord 29861 | If a nonempty finite friendship graph is k-regular, its order is k(k-1)+1. This corresponds to claim 3 in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". Variant of frrusgrord0 29860, using the definition RegUSGraph (df-rusgr 29082). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 26-May-2021.) (Proof shortened by AV, 12-Jan-2022.) |
β’ π = (VtxβπΊ) β β’ ((π β Fin β§ π β β ) β ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β (β―βπ) = ((πΎ Β· (πΎ β 1)) + 1))) | ||
Theorem | numclwwlk2lem1lem 29862 | Lemma for numclwwlk2lem1 29896. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-May-2021.) (Revised by AV, 15-Mar-2022.) |
β’ ((π β (VtxβπΊ) β§ π β (π WWalksN πΊ) β§ (lastSβπ) β (πβ0)) β (((π ++ β¨βπββ©)β0) = (πβ0) β§ ((π ++ β¨βπββ©)βπ) β (πβ0))) | ||
Theorem | 2clwwlklem 29863 | Lemma for clwwnonrepclwwnon 29865 and extwwlkfab 29872. (Contributed by Alexander van der Vekens, 18-Sep-2018.) (Revised by AV, 10-May-2022.) (Revised by AV, 30-Oct-2022.) |
β’ ((π β (π ClWWalksN πΊ) β§ π β (β€β₯β3)) β ((π prefix (π β 2))β0) = (πβ0)) | ||
Theorem | clwwnrepclwwn 29864 | If the initial vertex of a closed walk occurs another time in the walk, the walk starts with a closed walk. Notice that 3 β€ π is required, because for π = 2, (π€ prefix (π β 2)) = (π€ prefix 0) = β , but β (and anything else) is not a representation of an empty closed walk as word, see clwwlkn0 29548. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 30-Oct-2022.) |
β’ ((π β (β€β₯β3) β§ π β (π ClWWalksN πΊ) β§ (πβ(π β 2)) = (πβ0)) β (π prefix (π β 2)) β ((π β 2) ClWWalksN πΊ)) | ||
Theorem | clwwnonrepclwwnon 29865 | If the initial vertex of a closed walk occurs another time in the walk, the walk starts with a closed walk on this vertex. See also the remarks in clwwnrepclwwn 29864. (Contributed by AV, 24-Apr-2022.) (Revised by AV, 10-May-2022.) (Revised by AV, 30-Oct-2022.) |
β’ ((π β (β€β₯β3) β§ π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π) β (π prefix (π β 2)) β (π(ClWWalksNOnβπΊ)(π β 2))) | ||
Theorem | 2clwwlk2clwwlklem 29866 | Lemma for 2clwwlk2clwwlk 29870. (Contributed by AV, 27-Apr-2022.) |
β’ ((π β (β€β₯β3) β§ π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = (πβ0)) β (π substr β¨(π β 2), πβ©) β (π(ClWWalksNOnβπΊ)2)) | ||
Theorem | 2clwwlk 29867* | Value of operation πΆ, mapping a vertex v and an integer n greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v" according to definition 6 in [Huneke] p. 2. Such closed walks are "double loops" consisting of a closed (n-2)-walk v = v(0) ... v(n-2) = v and a closed 2-walk v = v(n-2) v(n-1) v(n) = v, see 2clwwlk2clwwlk 29870. (ππΆπ) is called the "set of double loops of length π on vertex π " in the following. (Contributed by Alexander van der Vekens, 14-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 20-Apr-2022.) |
β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) β β’ ((π β π β§ π β (β€β₯β2)) β (ππΆπ) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π}) | ||
Theorem | 2clwwlk2 29868* | The set (ππΆ2) of double loops of length 2 on a vertex π is equal to the set of closed walks with length 2 on π. Considered as "double loops", the first of the two closed walks/loops is degenerated, i.e., has length 0. (Contributed by AV, 18-Feb-2022.) (Revised by AV, 20-Apr-2022.) |
β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) β β’ (π β π β (ππΆ2) = (π(ClWWalksNOnβπΊ)2)) | ||
Theorem | 2clwwlkel 29869* | Characterization of an element of the value of operation πΆ, i.e., of a word being a double loop of length π on vertex π. (Contributed by Alexander van der Vekens, 24-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 20-Apr-2022.) |
β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) β β’ ((π β π β§ π β (β€β₯β2)) β (π β (ππΆπ) β (π β (π(ClWWalksNOnβπΊ)π) β§ (πβ(π β 2)) = π))) | ||
Theorem | 2clwwlk2clwwlk 29870* | An element of the value of operation πΆ, i.e., a word being a double loop of length π on vertex π, is composed of two closed walks. (Contributed by AV, 28-Apr-2022.) (Proof shortened by AV, 3-Nov-2022.) |
β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) β β’ ((π β π β§ π β (β€β₯β3)) β (π β (ππΆπ) β βπ β (π(ClWWalksNOnβπΊ)(π β 2))βπ β (π(ClWWalksNOnβπΊ)2)π = (π ++ π))) | ||
Theorem | numclwwlk1lem2foalem 29871 | Lemma for numclwwlk1lem2foa 29874. (Contributed by AV, 29-May-2021.) (Revised by AV, 1-Nov-2022.) |
β’ (((π β Word π β§ (β―βπ) = (π β 2)) β§ (π β π β§ π β π) β§ π β (β€β₯β3)) β ((((π ++ β¨βπββ©) ++ β¨βπββ©) prefix (π β 2)) = π β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 1)) = π β§ (((π ++ β¨βπββ©) ++ β¨βπββ©)β(π β 2)) = π)) | ||
Theorem | extwwlkfab 29872* | The set (ππΆπ) of double loops of length π on vertex π can be constructed from the set πΉ of closed walks on π with length smaller by 2 than the fixed length by appending a neighbor of the last vertex and afterwards the last vertex (which is the first vertex) itself ("walking forth and back" from the last vertex). 3 β€ π is required since for π = 2: πΉ = (π(ClWWalksNOnβπΊ)0) = β (see clwwlk0on0 29612 stating that a closed walk of length 0 is not represented as word), which would result in an empty set on the right hand side, but (ππΆπ) needs not be empty, see 2clwwlk2 29868. (Contributed by Alexander van der Vekens, 18-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 31-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) β β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3)) β (ππΆπ) = {π€ β (π ClWWalksN πΊ) β£ ((π€ prefix (π β 2)) β πΉ β§ (π€β(π β 1)) β (πΊ NeighbVtx π) β§ (π€β(π β 2)) = π)}) | ||
Theorem | extwwlkfabel 29873* | Characterization of an element of the set (ππΆπ), i.e., a double loop of length π on vertex π with a construction from the set πΉ of closed walks on π with length smaller by 2 than the fixed length by appending a neighbor of the last vertex and afterwards the last vertex (which is the first vertex) itself ("walking forth and back" from the last vertex). (Contributed by AV, 22-Feb-2022.) (Revised by AV, 31-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) β β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3)) β (π β (ππΆπ) β (π β (π ClWWalksN πΊ) β§ ((π prefix (π β 2)) β πΉ β§ (πβ(π β 1)) β (πΊ NeighbVtx π) β§ (πβ(π β 2)) = π)))) | ||
Theorem | numclwwlk1lem2foa 29874* | Going forth and back from the end of a (closed) walk: π represents the closed walk p0, ..., p(n-2), p0 = p(n-2). With π = p(n-2) = p0 and π = p(n-1), ((π ++ β¨βπββ©) ++ β¨βπββ©) represents the closed walk p0, ..., p(n-2), p(n-1), pn = p0 which is a double loop of length π on vertex π. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 5-Mar-2022.) (Proof shortened by AV, 2-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) β β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3)) β ((π β πΉ β§ π β (πΊ NeighbVtx π)) β ((π ++ β¨βπββ©) ++ β¨βπββ©) β (ππΆπ))) | ||
Theorem | numclwwlk1lem2f 29875* | π is a function, mapping a double loop of length π on vertex π to the ordered pair of the first loop and the successor of π in the second loop, which must be a neighbor of π. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 29-May-2021.) (Proof shortened by AV, 23-Feb-2022.) (Revised by AV, 31-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) & β’ π = (π’ β (ππΆπ) β¦ β¨(π’ prefix (π β 2)), (π’β(π β 1))β©) β β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3)) β π:(ππΆπ)βΆ(πΉ Γ (πΊ NeighbVtx π))) | ||
Theorem | numclwwlk1lem2fv 29876* | Value of the function π. (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 31-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) & β’ π = (π’ β (ππΆπ) β¦ β¨(π’ prefix (π β 2)), (π’β(π β 1))β©) β β’ (π β (ππΆπ) β (πβπ) = β¨(π prefix (π β 2)), (πβ(π β 1))β©) | ||
Theorem | numclwwlk1lem2f1 29877* | π is a 1-1 function. (Contributed by AV, 26-Sep-2018.) (Revised by AV, 29-May-2021.) (Proof shortened by AV, 23-Feb-2022.) (Revised by AV, 31-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) & β’ π = (π’ β (ππΆπ) β¦ β¨(π’ prefix (π β 2)), (π’β(π β 1))β©) β β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3)) β π:(ππΆπ)β1-1β(πΉ Γ (πΊ NeighbVtx π))) | ||
Theorem | numclwwlk1lem2fo 29878* | π is an onto function. (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 29-May-2021.) (Proof shortened by AV, 13-Feb-2022.) (Revised by AV, 31-Oct-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) & β’ π = (π’ β (ππΆπ) β¦ β¨(π’ prefix (π β 2)), (π’β(π β 1))β©) β β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3)) β π:(ππΆπ)βontoβ(πΉ Γ (πΊ NeighbVtx π))) | ||
Theorem | numclwwlk1lem2f1o 29879* | π is a 1-1 onto function. (Contributed by Alexander van der Vekens, 26-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 6-Mar-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) & β’ π = (π’ β (ππΆπ) β¦ β¨(π’ prefix (π β 2)), (π’β(π β 1))β©) β β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3)) β π:(ππΆπ)β1-1-ontoβ(πΉ Γ (πΊ NeighbVtx π))) | ||
Theorem | numclwwlk1lem2 29880* | The set of double loops of length π on vertex π and the set of closed walks of length less by 2 on π combined with the neighbors of π are equinumerous. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 31-Jul-2022.) (Proof shortened by AV, 3-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) β β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3)) β (ππΆπ) β (πΉ Γ (πΊ NeighbVtx π))) | ||
Theorem | numclwwlk1 29881* | Statement 9 in [Huneke] p. 2: "If n > 1, then the number of closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v is kf(n-2)". Since πΊ is k-regular, the vertex v(n-2) = v has k neighbors v(n-1), so there are k walks from v(n-2) = v to v(n) = v (via each of v's neighbors) completing each of the f(n-2) walks from v=v(0) to v(n-2)=v. This theorem holds even for k=0, but not for n=2, since πΉ = β , but (ππΆ2), the set of closed walks with length 2 on π, see 2clwwlk2 29868, needs not be β in this case. This is because of the special definition of πΉ and the usage of words to represent (closed) walks, and does not contradict Huneke's statement, which would read "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)", where f(0)=1 is the number of empty closed walks on v, see numclwlk1lem1 29889. If the general representation of (closed) walk is used, Huneke's statement can be proven even for n = 2, see numclwlk1 29891. This case, however, is not required to prove the friendship theorem. (Contributed by Alexander van der Vekens, 26-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 6-Mar-2022.) (Proof shortened by AV, 31-Jul-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) & β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) β β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3))) β (β―β(ππΆπ)) = (πΎ Β· (β―βπΉ))) | ||
Theorem | clwwlknonclwlknonf1o 29882* | πΉ is a bijection between the two representations of closed walks of a fixed positive length on a fixed vertex. (Contributed by AV, 26-May-2022.) (Proof shortened by AV, 7-Aug-2022.) (Revised by AV, 1-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ π = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)} & β’ πΉ = (π β π β¦ ((2nd βπ) prefix (β―β(1st βπ)))) β β’ ((πΊ β USPGraph β§ π β π β§ π β β) β πΉ:πβ1-1-ontoβ(π(ClWWalksNOnβπΊ)π)) | ||
Theorem | clwwlknonclwlknonen 29883* | The sets of the two representations of closed walks of a fixed positive length on a fixed vertex are equinumerous. (Contributed by AV, 27-May-2022.) (Proof shortened by AV, 3-Nov-2022.) |
β’ ((πΊ β USPGraph β§ π β (VtxβπΊ) β§ π β β) β {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)} β (π(ClWWalksNOnβπΊ)π)) | ||
Theorem | dlwwlknondlwlknonf1olem1 29884 | Lemma 1 for dlwwlknondlwlknonf1o 29885. (Contributed by AV, 29-May-2022.) (Revised by AV, 1-Nov-2022.) |
β’ (((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β (β€β₯β2)) β (((2nd βπ) prefix (β―β(1st βπ)))β(π β 2)) = ((2nd βπ)β(π β 2))) | ||
Theorem | dlwwlknondlwlknonf1o 29885* | πΉ is a bijection between the two representations of double loops of a fixed positive length on a fixed vertex. (Contributed by AV, 30-May-2022.) (Revised by AV, 1-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ π = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β(π β 2)) = π)} & β’ π· = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π} & β’ πΉ = (π β π β¦ ((2nd βπ) prefix (β―β(1st βπ)))) β β’ ((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2)) β πΉ:πβ1-1-ontoβπ·) | ||
Theorem | dlwwlknondlwlknonen 29886* | The sets of the two representations of double loops of a fixed length on a fixed vertex are equinumerous. (Contributed by AV, 30-May-2022.) (Proof shortened by AV, 3-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ π = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β(π β 2)) = π)} & β’ π· = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π} β β’ ((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2)) β π β π·) | ||
Theorem | wlkl0 29887* | There is exactly one walk of length 0 on each vertex π. (Contributed by AV, 4-Jun-2022.) |
β’ π = (VtxβπΊ) β β’ (π β π β {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)} = {β¨β , {β¨0, πβ©}β©}) | ||
Theorem | clwlknon2num 29888* | There are k walks of length 2 on each vertex π in a k-regular simple graph. Variant of clwwlknon2num 29625, using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022.) |
β’ π = (VtxβπΊ) β β’ ((π β Fin β§ πΊ RegUSGraph πΎ β§ π β π) β (β―β{π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = 2 β§ ((2nd βπ€)β0) = π)}) = πΎ) | ||
Theorem | numclwlk1lem1 29889* | Lemma 1 for numclwlk1 29891 (Statement 9 in [Huneke] p. 2 for n=2): "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)". (Contributed by AV, 23-May-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β(π β 2)) = π)} & β’ πΉ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = (π β 2) β§ ((2nd βπ€)β0) = π)} β β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π = 2)) β (β―βπΆ) = (πΎ Β· (β―βπΉ))) | ||
Theorem | numclwlk1lem2 29890* | Lemma 2 for numclwlk1 29891 (Statement 9 in [Huneke] p. 2 for n>2). This theorem corresponds to numclwwlk1 29881, using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β(π β 2)) = π)} & β’ πΉ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = (π β 2) β§ ((2nd βπ€)β0) = π)} β β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3))) β (β―βπΆ) = (πΎ Β· (β―βπΉ))) | ||
Theorem | numclwlk1 29891* | Statement 9 in [Huneke] p. 2: "If n > 1, then the number of closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v is kf(n-2)". Since πΊ is k-regular, the vertex v(n-2) = v has k neighbors v(n-1), so there are k walks from v(n-2) = v to v(n) = v (via each of v's neighbors) completing each of the f(n-2) walks from v=v(0) to v(n-2)=v. This theorem holds even for k=0. (Contributed by AV, 23-May-2022.) |
β’ π = (VtxβπΊ) & β’ πΆ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β(π β 2)) = π)} & β’ πΉ = {π€ β (ClWalksβπΊ) β£ ((β―β(1st βπ€)) = (π β 2) β§ ((2nd βπ€)β0) = π)} β β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β2))) β (β―βπΆ) = (πΎ Β· (β―βπΉ))) | ||
Theorem | numclwwlkovh0 29892* | Value of operation π», mapping a vertex π£ and an integer π greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) ... with v(n-2) =/= v" according to definition 7 in [Huneke] p. 2. (Contributed by AV, 1-May-2022.) |
β’ π» = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) β β’ ((π β π β§ π β (β€β₯β2)) β (ππ»π) = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π}) | ||
Theorem | numclwwlkovh 29893* | Value of operation π», mapping a vertex π£ and an integer π greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) ... with v(n-2) =/= v" according to definition 7 in [Huneke] p. 2. Definition of ClWWalksNOn resolved. (Contributed by Alexander van der Vekens, 26-Aug-2018.) (Revised by AV, 30-May-2021.) (Revised by AV, 1-May-2022.) |
β’ π» = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) β β’ ((π β π β§ π β (β€β₯β2)) β (ππ»π) = {π€ β (π ClWWalksN πΊ) β£ ((π€β0) = π β§ (π€β(π β 2)) β (π€β0))}) | ||
Theorem | numclwwlkovq 29894* | Value of operation π, mapping a vertex π£ and a positive integer π to the not closed walks v(0) ... v(n) of length π from a fixed vertex π£ = v(0). "Not closed" means v(n) =/= v(0). Remark: π β β0 would not be useful: numclwwlkqhash 29895 would not hold, because (πΎβ0) = 1! (Contributed by Alexander van der Vekens, 27-Sep-2018.) (Revised by AV, 30-May-2021.) |
β’ π = (VtxβπΊ) & β’ π = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) β β’ ((π β π β§ π β β) β (πππ) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (lastSβπ€) β π)}) | ||
Theorem | numclwwlkqhash 29895* | In a πΎ-regular graph, the size of the set of walks of length π starting with a fixed vertex π and ending not at this vertex is the difference between πΎ to the power of π and the size of the set of closed walks of length π on vertex π. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 30-May-2021.) (Revised by AV, 5-Mar-2022.) (Proof shortened by AV, 7-Jul-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) β β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β)) β (β―β(πππ)) = ((πΎβπ) β (β―β(π(ClWWalksNOnβπΊ)π)))) | ||
Theorem | numclwwlk2lem1 29896* | In a friendship graph, for each walk of length π starting at a fixed vertex π£ and ending not at this vertex, there is a unique vertex so that the walk extended by an edge to this vertex and an edge from this vertex to the first vertex of the walk is a value of operation π». If the walk is represented as a word, it is sufficient to add one vertex to the word to obtain the closed walk contained in the value of operation π», since in a word representing a closed walk the starting vertex is not repeated at the end. This theorem generally holds only for friendship graphs, because these guarantee that for the first and last vertex there is a (unique) third vertex "in between". (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 30-May-2021.) (Revised by AV, 1-May-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) & β’ π» = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) β β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β (π β (πππ) β β!π£ β π (π ++ β¨βπ£ββ©) β (ππ»(π + 2)))) | ||
Theorem | numclwlk2lem2f 29897* | π is a function mapping the "closed (n+2)-walks v(0) ... v(n-2) v(n-1) v(n) v(n+1) v(n+2) starting at π = v(0) = v(n+2) with v(n) =/= X" to the words representing the prefix v(0) ... v(n-2) v(n-1) v(n) of the walk. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 31-May-2021.) (Proof shortened by AV, 23-Mar-2022.) (Revised by AV, 1-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) & β’ π» = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) & β’ π = (π₯ β (ππ»(π + 2)) β¦ (π₯ prefix (π + 1))) β β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β π :(ππ»(π + 2))βΆ(πππ)) | ||
Theorem | numclwlk2lem2fv 29898* | Value of the function π . (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 31-May-2021.) (Revised by AV, 1-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) & β’ π» = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) & β’ π = (π₯ β (ππ»(π + 2)) β¦ (π₯ prefix (π + 1))) β β’ ((π β π β§ π β β) β (π β (ππ»(π + 2)) β (π βπ) = (π prefix (π + 1)))) | ||
Theorem | numclwlk2lem2f1o 29899* | π is a 1-1 onto function. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Proof shortened by AV, 17-Mar-2022.) (Revised by AV, 1-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) & β’ π» = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) & β’ π = (π₯ β (ππ»(π + 2)) β¦ (π₯ prefix (π + 1))) β β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β π :(ππ»(π + 2))β1-1-ontoβ(πππ)) | ||
Theorem | numclwwlk2lem3 29900* | In a friendship graph, the size of the set of walks of length π starting with a fixed vertex π and ending not at this vertex equals the size of the set of all closed walks of length (π + 2) starting at this vertex π and not having this vertex as last but 2 vertex. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 31-May-2021.) (Proof shortened by AV, 3-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ π = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) & β’ π» = (π£ β π, π β (β€β₯β2) β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) β β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β (β―β(πππ)) = (β―β(ππ»(π + 2)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |