Home | Metamath
Proof Explorer Theorem List (p. 265 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 1hevtxdg0 26401 | The vertex degree of vertex 𝐷 in a graph 𝐺 with only one hyperedge 𝐸 is 0 if 𝐷 is not incident with the edge 𝐸. (Contributed by AV, 2-Mar-2021.) |
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) & ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → 𝐷 ∉ 𝐸) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 0) | ||
Theorem | 1hevtxdg1 26402 | The vertex degree of vertex 𝐷 in a graph 𝐺 with only one hyperedge 𝐸 (not being a loop) is 1 if 𝐷 is incident with the edge 𝐸. (Contributed by AV, 2-Mar-2021.) (Proof shortened by AV, 17-Apr-2021.) |
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) & ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝐸) & ⊢ (𝜑 → 2 ≤ (#‘𝐸)) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 1) | ||
Theorem | 1hegrvtxdg1 26403 | The vertex degree of a graph with one hyperedge, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) & ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1) | ||
Theorem | 1hegrvtxdg1r 26404 | The vertex degree of a graph with one hyperedge, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) & ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1) | ||
Theorem | 1egrvtxdg1 26405 | The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1) | ||
Theorem | 1egrvtxdg1r 26406 | The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1) | ||
Theorem | 1egrvtxdg0 26407 | The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ≠ 𝐷) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐷}〉}) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 0) | ||
Theorem | p1evtxdeqlem 26408 | Lemma for p1evtxdeq 26409 and p1evtxdp1 26410. (Contributed by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {〈𝐾, 𝐸〉})) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐾 ∉ dom 𝐼) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 ((VtxDeg‘〈𝑉, {〈𝐾, 𝐸〉}〉)‘𝑈))) | ||
Theorem | p1evtxdeq 26409 | If an edge 𝐸 which does not contain vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is the same in both graphs. (Contributed by AV, 2-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {〈𝐾, 𝐸〉})) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐾 ∉ dom 𝐼) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → 𝑈 ∉ 𝐸) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = ((VtxDeg‘𝐺)‘𝑈)) | ||
Theorem | p1evtxdp1 26410 | If an edge 𝐸 (not being a loop) which contains vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is increased by 1. (Contributed by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {〈𝐾, 𝐸〉})) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐾 ∉ dom 𝐼) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) & ⊢ (𝜑 → 𝑈 ∈ 𝐸) & ⊢ (𝜑 → 2 ≤ (#‘𝐸)) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 1)) | ||
Theorem | uspgrloopvtx 26411 | The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26141). (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) | ||
Theorem | uspgrloopvtxel 26412 | A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26141). (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ (Vtx‘𝐺)) | ||
Theorem | uspgrloopiedg 26413 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26141) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) | ||
Theorem | uspgrloopedg 26414 | The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26141) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (Edg‘𝐺) = {{𝑁}}) | ||
Theorem | uspgrloopnb0 26415 | In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26141), the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = ∅) | ||
Theorem | uspgrloopvd2 26416 | The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 26141), the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑁) = 2) | ||
Theorem | umgr2v2evtx 26417 | The set of vertices in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) | ||
Theorem | umgr2v2evtxel 26418 | A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ (Vtx‘𝐺)) | ||
Theorem | umgr2v2eiedg 26419 | The edge function in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}) | ||
Theorem | umgr2v2eedg 26420 | The set of edges in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Edg‘𝐺) = {{𝐴, 𝐵}}) | ||
Theorem | umgr2v2e 26421 | A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph ) | ||
Theorem | umgr2v2enb1 26422 | In a multigraph with two edges connecting the same two vertices, each of the vertices has one neighbor. (Contributed by AV, 18-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 NeighbVtx 𝐴) = {𝐵}) | ||
Theorem | umgr2v2evd2 26423 | In a multigraph with two edges connecting the same two vertices, each of the vertices has degree 2. (Contributed by AV, 18-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈0, {𝐴, 𝐵}〉, 〈1, {𝐴, 𝐵}〉}〉 ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((VtxDeg‘𝐺)‘𝐴) = 2) | ||
Theorem | hashnbusgrvd 26424 | In a simple graph, the number of neighbors of a vertex is the degree of this vertex. This theorem does not hold for (simple) pseudographs, because a vertex connected with itself only by a loop has no neighbors, see uspgrloopnb0 26415, but degree 2, see uspgrloopvd2 26416. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 26422, but also degree 2, see umgr2v2evd2 26423. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (#‘(𝐺 NeighbVtx 𝑈)) = ((VtxDeg‘𝐺)‘𝑈)) | ||
Theorem | usgruvtxvdb 26425 | In a finite simple graph with n vertices a vertex is universal iff the vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (𝑈 ∈ (UnivVtx‘𝐺) ↔ ((VtxDeg‘𝐺)‘𝑈) = ((#‘𝑉) − 1))) | ||
Theorem | vdiscusgrb 26426* | A finite simple graph with n vertices is complete iff every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 22-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (𝐺 ∈ ComplUSGraph ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = ((#‘𝑉) − 1))) | ||
Theorem | vdiscusgr 26427* | In a finite complete simple graph with n vertices every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = ((#‘𝑉) − 1) → 𝐺 ∈ ComplUSGraph)) | ||
Theorem | vtxdusgradjvtx 26428* | The degree of a vertex in a simple graph is the number of vertices adjacent to this vertex. (Contributed by Alexander van der Vekens, 9-Jul-2018.) (Revised by AV, 23-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = (#‘{𝑣 ∈ 𝑉 ∣ {𝑈, 𝑣} ∈ 𝐸})) | ||
Theorem | usgrvd0nedg 26429* | If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 16-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (((VtxDeg‘𝐺)‘𝑈) = 0 → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸)) | ||
Theorem | uhgrvd00 26430* | If every vertex in a hypergraph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → 𝐸 = ∅)) | ||
Theorem | usgrvd00 26431* | If every vertex in a simple graph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → 𝐸 = ∅)) | ||
Theorem | vdegp1ai 26432* | The induction step for a vertex degree calculation. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑌} to the edge set, where 𝑋 ≠ 𝑈 ≠ 𝑌, yields degree 𝑃 as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 ∈ 𝑉 & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} & ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃 & ⊢ (Vtx‘𝐹) = 𝑉 & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑌 ≠ 𝑈 & ⊢ (iEdg‘𝐹) = (𝐼 ++ 〈“{𝑋, 𝑌}”〉) ⇒ ⊢ ((VtxDeg‘𝐹)‘𝑈) = 𝑃 | ||
Theorem | vdegp1bi 26433* | The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑈, 𝑋} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 ∈ 𝑉 & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} & ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃 & ⊢ (Vtx‘𝐹) = 𝑉 & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ (iEdg‘𝐹) = (𝐼 ++ 〈“{𝑈, 𝑋}”〉) ⇒ ⊢ ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1) | ||
Theorem | vdegp1ci 26434* | The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑈} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑈 ∈ 𝑉 & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} & ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃 & ⊢ (Vtx‘𝐹) = 𝑉 & ⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑈 & ⊢ (iEdg‘𝐹) = (𝐼 ++ 〈“{𝑋, 𝑈}”〉) ⇒ ⊢ ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1) | ||
Theorem | vtxdginducedm1lem1 26435 | Lemma 1 for vtxdginducedm1 26439: the edge function in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ (iEdg‘𝑆) = 𝑃 | ||
Theorem | vtxdginducedm1lem2 26436* | Lemma 2 for vtxdginducedm1 26439: the domain of the edge function in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ dom (iEdg‘𝑆) = 𝐼 | ||
Theorem | vtxdginducedm1lem3 26437* | Lemma 3 for vtxdginducedm1 26439: an edge in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ (𝐻 ∈ 𝐼 → ((iEdg‘𝑆)‘𝐻) = (𝐸‘𝐻)) | ||
Theorem | vtxdginducedm1lem4 26438* | Lemma 4 for vtxdginducedm1 26439. (Contributed by AV, 17-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (𝑊 ∈ (𝑉 ∖ {𝑁}) → (#‘{𝑘 ∈ 𝐽 ∣ (𝐸‘𝑘) = {𝑊}}) = 0) | ||
Theorem | vtxdginducedm1 26439* | The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 17-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) +𝑒 (#‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)})) | ||
Theorem | vtxdginducedm1fi 26440* | The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 of finite size obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 18-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (𝐸 ∈ Fin → ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) + (#‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)}))) | ||
Theorem | finsumvtxdg2ssteplem1 26441* | Lemma for finsumvtxdg2sstep 26445. (Contributed by AV, 15-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (#‘𝐸) = ((#‘𝑃) + (#‘𝐽))) | ||
Theorem | finsumvtxdg2ssteplem2 26442* | Lemma for finsumvtxdg2sstep 26445. (Contributed by AV, 12-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((VtxDeg‘𝐺)‘𝑁) = ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) | ||
Theorem | finsumvtxdg2ssteplem3 26443* | Lemma for finsumvtxdg2sstep 26445. (Contributed by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(#‘{𝑖 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑖)}) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (#‘𝐽)) | ||
Theorem | finsumvtxdg2ssteplem4 26444* | Lemma for finsumvtxdg2sstep 26445. (Contributed by AV, 12-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 & ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)} ⇒ ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((#‘𝐽) + (#‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) = (2 · ((#‘𝑃) + (#‘𝐽)))) | ||
Theorem | finsumvtxdg2sstep 26445* | Induction step of finsumvtxdg2size 26446: In a finite pseudograph of finite size, the sum of the degrees of all vertices of the pseudograph is twice the size of the pseudograph if the sum of the degrees of all vertices of the subgraph of the pseudograph not containing one of the vertices is twice the size of the subgraph. (Contributed by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐾 = (𝑉 ∖ {𝑁}) & ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑃 = (𝐸 ↾ 𝐼) & ⊢ 𝑆 = 〈𝐾, 𝑃〉 ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((𝑃 ∈ Fin → Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (#‘𝑃))) → Σ𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = (2 · (#‘𝐸)))) | ||
Theorem | finsumvtxdg2size 26446* |
The sum of the degrees of all vertices of a finite pseudograph of finite
size is twice the size of the pseudograph. See equation (1) in section
I.1 in [Bollobas] p. 4. Here, the
"proof" is simply the statement
"Since each edge has two endvertices, the sum of the degrees is
exactly
twice the number of edges". The formal proof of this theorem (for
pseudographs) is much more complicated, taking also the used auxiliary
theorems into account. The proof for a (finite) simple graph (see
fusgr1th 26447) would be shorter, but nevertheless still
laborious.
Although this theorem would hold also for infinite pseudographs and
pseudographs of infinite size, the proof of this most general version
(see theorem "sumvtxdg2size" below) would require many more
auxiliary
theorems (e.g., the extension of the sum Σ
over an arbitrary
set).
I dedicate this theorem and its proof to Norman Megill, who deceased too early on December 9, 2021. This proof is an example for the rigor which was the main motivation for Norman Megill to invent and develop Metamath, see section 1.1.6 "Rigor" on page 19 of the Metamath book: "... it is usually assumed in mathematical literature that the person reading the proof is a mathematician familiar with the specialty being described, and that the missing steps are obvious to such a reader or at least the reader is capable of filling them in." I filled in the missing steps of Bollobas' proof as Norm would have liked it... (Contributed by Alexander van der Vekens, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (#‘𝐼))) | ||
Theorem | fusgr1th 26447* | The sum of the degrees of all vertices of a finite simple graph is twice the size of the graph. See equation (1) in section I.1 in [Bollobas] p. 4. Also known as the "First Theorem of Graph Theory" (see https://charlesreid1.com/wiki/First_Theorem_of_Graph_Theory). (Contributed by AV, 26-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (#‘𝐼))) | ||
Theorem | finsumvtxdgeven 26448* | The sum of the degrees of all vertices of a finite pseudograph of finite size is even. See equation (2) in section I.1 in [Bollobas] p. 4, where it is also called the handshaking lemma. (Contributed by AV, 22-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → 2 ∥ Σ𝑣 ∈ 𝑉 (𝐷‘𝑣)) | ||
Theorem | vtxdgoddnumeven 26449* | The number of vertices of odd degree is even in a finite pseudograph of finite size. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 22-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → 2 ∥ (#‘{𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ (𝐷‘𝑣)})) | ||
Theorem | fusgrvtxdgonume 26450* | The number of vertices of odd degree is even in a finite simple graph. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 27-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → 2 ∥ (#‘{𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ (𝐷‘𝑣)})) | ||
With df-rgr 26453 and df-rusgr 26454, k-regularity of a (simple) graph is defined as predicate RegGraph resp. RegUSGraph. Instead of defining a predicate, an alternative could have been to define a function that maps an extended nonnegative integer to the class of "graphs" in which every vertex has the extended nonnegative integer as degree: RegGraph = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘}). This function, however, would not be defined at least for 𝑘 = 0 (see rgrx0nd 26490), because {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} is not a set (see rgrprcx 26488). It is expected that this function is not defined for every 𝑘 ∈ ℕ0* (how could this be proven?). | ||
Syntax | crgr 26451 | Extend class notation to include the class of all regular graphs. |
class RegGraph | ||
Syntax | crusgr 26452 | Extend class notation to include the class of all regular simple graphs. |
class RegUSGraph | ||
Definition | df-rgr 26453* | Define the "k-regular" predicate, which is true for a "graph" being k-regular: read 𝐺 RegGraph 𝐾 as "𝐺 is 𝐾-regular" or "𝐺 is a 𝐾-regular graph". Note that 𝐾 is allowed to be positive infinity (𝐾 ∈ ℕ0*), as proposed by GL. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ RegGraph = {〈𝑔, 𝑘〉 ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)} | ||
Definition | df-rusgr 26454* | Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read 𝐺 RegUSGraph 𝐾 as 𝐺 is a 𝐾-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ RegUSGraph = {〈𝑔, 𝑘〉 ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)} | ||
Theorem | isrgr 26455* | The property of a class being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGraph 𝐾 ↔ (𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))) | ||
Theorem | rgrprop 26456* | The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 RegGraph 𝐾 → (𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)) | ||
Theorem | isrusgr 26457 | The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾))) | ||
Theorem | rusgrprop 26458 | The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾)) | ||
Theorem | rusgrrgr 26459 | A k-regular simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 RegGraph 𝐾) | ||
Theorem | rusgrusgr 26460 | A k-regular simple graph is a simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.) |
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph ) | ||
Theorem | finrusgrfusgr 26461 | A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph ) | ||
Theorem | isrusgr0 26462* | The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))) | ||
Theorem | rusgrprop0 26463* | The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)) | ||
Theorem | usgreqdrusgr 26464* | If all vertices in a simple graph have the same degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾) → 𝐺 RegUSGraph 𝐾) | ||
Theorem | fusgrregdegfi 26465* | In a nonempty finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.) (Revised by AV, 19-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 → 𝐾 ∈ ℕ0)) | ||
Theorem | fusgrn0eqdrusgr 26466* | If all vertices in a nonempty finite simple graph have the same (finite) degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 → 𝐺 RegUSGraph 𝐾)) | ||
Theorem | frusgrnn0 26467 | In a nonempty finite k-regular simple graph, the degree of each vertex is finite. (Contributed by AV, 7-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈ ℕ0) | ||
Theorem | 0edg0rgr 26468 | A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (iEdg‘𝐺) = ∅) → 𝐺 RegGraph 0) | ||
Theorem | uhgr0edg0rgr 26469 | A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ (Edg‘𝐺) = ∅) → 𝐺 RegGraph 0) | ||
Theorem | uhgr0edg0rgrb 26470 | A hypergraph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.) |
⊢ (𝐺 ∈ UHGraph → (𝐺 RegGraph 0 ↔ (Edg‘𝐺) = ∅)) | ||
Theorem | usgr0edg0rusgr 26471 | A simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 19-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
⊢ (𝐺 ∈ USGraph → (𝐺 RegUSGraph 0 ↔ (Edg‘𝐺) = ∅)) | ||
Theorem | 0vtxrgr 26472* | A null graph (with no vertices) is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegGraph 𝑘) | ||
Theorem | 0vtxrusgr 26473* | A graph with no vertices and an empty edge function is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘) | ||
Theorem | 0uhgrrusgr 26474* | The null graph as hypergraph is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘) | ||
Theorem | 0grrusgr 26475 | The null graph represented by an empty set is a k-regular simple graph for every k. (Contributed by AV, 26-Dec-2020.) |
⊢ ∀𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘 | ||
Theorem | 0grrgr 26476 | The null graph represented by an empty set is k-regular for every k. (Contributed by AV, 26-Dec-2020.) |
⊢ ∀𝑘 ∈ ℕ0* ∅ RegGraph 𝑘 | ||
Theorem | cusgrrusgr 26477 | A complete simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝐺 RegUSGraph ((#‘𝑉) − 1)) | ||
Theorem | cusgrm1rusgr 26478 | A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for 𝑘 ∈ ℤ, then the assumption 𝑉 ≠ ∅ could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ((#‘𝑉) − 1))) | ||
Theorem | rusgrpropnb 26479* | The properties of a k-regular simple graph expressed with neighbors. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 26-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (#‘(𝐺 NeighbVtx 𝑣)) = 𝐾)) | ||
Theorem | rusgrpropedg 26480* | The properties of a k-regular simple graph expressed with edges. (Contributed by AV, 23-Dec-2020.) (Revised by AV, 27-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (#‘{𝑒 ∈ (Edg‘𝐺) ∣ 𝑣 ∈ 𝑒}) = 𝐾)) | ||
Theorem | rusgrpropadjvtx 26481* | The properties of a k-regular simple graph expressed with adjacent vertices. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 27-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (#‘{𝑘 ∈ 𝑉 ∣ {𝑣, 𝑘} ∈ (Edg‘𝐺)}) = 𝐾)) | ||
Theorem | rusgrnumwrdl2 26482* | In a k-regular simple graph, the number of edges resp. walks of length 1 (represented as words of length 2) starting at a fixed vertex is k. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 6-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ Word 𝑉 ∣ ((#‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))}) = 𝐾) | ||
Theorem | rusgr1vtxlem 26483* | Lemma for rusgr1vtx 26484. (Contributed by AV, 27-Dec-2020.) |
⊢ (((∀𝑣 ∈ 𝑉 (#‘𝐴) = 𝐾 ∧ ∀𝑣 ∈ 𝑉 𝐴 = ∅) ∧ (𝑉 ∈ 𝑊 ∧ (#‘𝑉) = 1)) → 𝐾 = 0) | ||
Theorem | rusgr1vtx 26484 | If a k-regular simple graph has only one vertex, then k must be 0. (Contributed by Alexander van der Vekens, 4-Sep-2018.) (Revised by AV, 27-Dec-2020.) |
⊢ (((#‘(Vtx‘𝐺)) = 1 ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 = 0) | ||
Theorem | rgrusgrprc 26485* | The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ {𝑔 ∈ USGraph ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V | ||
Theorem | rusgrprc 26486 | The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ {𝑔 ∣ 𝑔 RegUSGraph 0} ∉ V | ||
Theorem | rgrprc 26487 | The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ {𝑔 ∣ 𝑔 RegGraph 0} ∉ V | ||
Theorem | rgrprcx 26488* | The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.) |
⊢ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V | ||
Theorem | rgrx0ndm 26489* | 0 is not in the domain of the potentially alternatively defined vertex degree function. (Contributed by AV, 28-Dec-2020.) |
⊢ 𝑅 = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘}) ⇒ ⊢ 0 ∉ dom 𝑅 | ||
Theorem | rgrx0nd 26490* | The potentially alternatively defined vertex degree function is not defined for 0. (Contributed by AV, 28-Dec-2020.) |
⊢ 𝑅 = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘}) ⇒ ⊢ (𝑅‘0) = ∅ | ||
A "walk" within a graph is usually defined for simple graphs, multigraphs or even pseudographs as "alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. This definition requires the edges to connect two vertices at most (loops are also allowed: if e(i) is a loop, then x(i-1) = x(i)). For hypergraphs containing hyperedges (i.e. edges connecting more than two vertices), however, a more general definition is needed. Two approaches for a definition applicable for arbitrary hypergraphs are used in the literature: "walks on the vertex level" and "walks on the edge level" (see Aksoy, Joslyn, Marrero, Praggastis, Purvine: "Hypernetwork science via high-order hypergraph walks", June 2020, https://doi.org/10.1140/epjds/s13688-020-00231-0): "walks on the edge level": For a positive integer s, an s-walk of length k between hyperedges f and g is a sequence of hyperedges, f=e(0), e(1), ... , e(k)=g, where for j=1, ... , k, e(j-1) =/= e(j) and e(j-1) and e(j) have at least s vertices in common (according to Aksoy et al.). "walks on the vertex level": For a positive integer s, an s-walk of length k between vertices a and b is a sequence of vertices, a=v(0), v(1), ... , v(k)=b, where for j=1, ... , k, v(j-1) and v(j) are connected by at least s edges (analogous to Aksoy et al.). There are two imperfections for the definition for "walks on the edge level": one is that a walk of length 1 consists of two edges (or a walk of length 0 consists of one edge), whereas a walk of length 1 on the vertex level consists of two vertices and one edge (or a walk of length 0 consists of one vertex and no edge). The other is that edges, especially loops, can be traversed only once (and not repeatedly) because of the condition e(j-1) =/= e(j). The latter is avoided in the definition for EdgWalks, see df-ewlks 26494. To be compatible with the (usual) definition of walks for pseudographs, walks also suitable for arbitrary hypergraphs are defined "on the vertex level" in the following as Walks, see df-wlks 26495, restricting s to 1. wlk1ewlk 26536 shows that such a 1-walk "on the vertex level" induces a 1-walk "on the edge level". | ||
Syntax | cewlks 26491 | Extend class notation with s-walks "on the edge level" (of a hypergraph). |
class EdgWalks | ||
Syntax | cwlks 26492 | Extend class notation with walks (i.e. 1-walks) (of a hypergraph). |
class Walks | ||
Syntax | cwlkson 26493 | Extend class notation with walks between two vertices (within a graph). |
class WalksOn | ||
Definition | df-ewlks 26494* | Define the set of all s-walks of edges (in a hypergraph) corresponding to s-walks "on the edge level" discussed in Aksoy et al. For an extended nonnegative integer s, an s-walk is a sequence of hyperedges, e(0), e(1), ... , e(k), where e(j-1) and e(j) have at least s vertices in common (for j=1, ... , k). In contrast to the definition in Aksoy et al., 𝑠 = 0 (a 0-walk is an arbitrary sequence of hyperedges) and 𝑠 = +∞ (then the number of common vertices of two adjacent hyperedges must be infinite) are allowed. Furthermore, it is not forbidden that adjacent hyperedges are equal. (Contributed by AV, 4-Jan-2021.) |
⊢ EdgWalks = (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑠 ≤ (#‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))}) | ||
Definition | df-wlks 26495* |
Define the set of all walks (in a hypergraph). Such walks correspond to
the s-walks "on the vertex level" (with s = 1), and also to
1-walks "on
the edge level" (see wlk1walk 26535) discussed in Aksoy et al. The
predicate 𝐹(Walks‘𝐺)𝑃 can be read as "The pair
〈𝐹, 𝑃〉 represents a walk in a graph
𝐺", see also iswlk 26506.
The condition {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘)) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. (𝑝‘𝑘) = (𝑝‘(𝑘 + 1)) should be allowed only if there is a loop at (𝑝‘𝑘). Otherwise, C would be fulfilled by each edge containing (𝑝‘𝑘). According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by AV, 30-Dec-2020.) |
⊢ Walks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))}) | ||
Definition | df-wlkson 26496* | Define the collection of walks with particular endpoints (in a hypergraph). The predicate 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 can be read as "The pair 〈𝐹, 𝑃〉 represents a walk from vertex 𝐴 to vertex 𝐵 in a graph 𝐺", see also iswlkon 26553. This corresponds to the "x0-x(l)-walks", see Definition in [Bollobas] p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
⊢ WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) | ||
Theorem | ewlksfval 26497* | The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*) → (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))}) | ||
Theorem | isewlk 26498* | Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈) → (𝐹 ∈ (𝐺 EdgWalks 𝑆) ↔ (𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘))))))) | ||
Theorem | ewlkprop 26499* | Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | ewlkinedg 26500 | The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝐾 ∈ (1..^(#‘𝐹))) → 𝑆 ≤ (#‘((𝐼‘(𝐹‘(𝐾 − 1))) ∩ (𝐼‘(𝐹‘𝐾))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |