![]() |
Metamath
Proof Explorer Theorem List (p. 273 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-cplgr 27201 | Define the class of all complete "graphs". A class/graph is called complete if every pair of distinct vertices is connected by an edge, i.e., each vertex has all other vertices as neighbors or, in other words, each vertex is a universal vertex. (Contributed by AV, 24-Oct-2020.) (Revised by TA, 15-Feb-2022.) |
⊢ ComplGraph = {𝑔 ∣ (UnivVtx‘𝑔) = (Vtx‘𝑔)} | ||
Definition | df-cusgr 27202 | Define the class of all complete simple graphs. A simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge, see definition in section 1.1 of [Diestel] p. 3. In contrast, the definition in section I.1 of [Bollobas] p. 3 is based on the size of (finite) complete graphs, see cusgrsize 27244. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.) (Revised by BJ, 14-Feb-2022.) |
⊢ ComplUSGraph = (USGraph ∩ ComplGraph) | ||
Theorem | cplgruvtxb 27203 | A graph 𝐺 is complete iff each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 15-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ (UnivVtx‘𝐺) = 𝑉)) | ||
Theorem | prcliscplgr 27204* | A proper class (representing a null graph, see vtxvalprc 26838) has the property of a complete graph (see also cplgr0v 27217), but cannot be an element of ComplGraph, of course. Because of this, a sethood antecedent like 𝐺 ∈ 𝑊 is necessary in the following theorems like iscplgr 27205. (Contributed by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (¬ 𝐺 ∈ V → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺)) | ||
Theorem | iscplgr 27205* | The property of being a complete graph. (Contributed by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))) | ||
Theorem | iscplgrnb 27206* | A graph is complete iff all vertices are neighbors of all vertices. (Contributed by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))) | ||
Theorem | iscplgredg 27207* | A graph 𝐺 is complete iff all vertices are connected with each other by (at least) one edge. (Contributed by AV, 10-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})∃𝑒 ∈ 𝐸 {𝑣, 𝑛} ⊆ 𝑒)) | ||
Theorem | iscusgr 27208 | The property of being a complete simple graph. (Contributed by AV, 1-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph)) | ||
Theorem | cusgrusgr 27209 | A complete simple graph is a simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph) | ||
Theorem | cusgrcplgr 27210 | A complete simple graph is a complete graph. (Contributed by AV, 1-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph → 𝐺 ∈ ComplGraph) | ||
Theorem | iscusgrvtx 27211* | A simple graph is complete iff all vertices are uniuversal. (Contributed by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))) | ||
Theorem | cusgruvtxb 27212 | A simple graph is complete iff the set of vertices is the set of universal vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by Alexander van der Vekens, 18-Jan-2018.) (Revised by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (𝐺 ∈ ComplUSGraph ↔ (UnivVtx‘𝐺) = 𝑉)) | ||
Theorem | iscusgredg 27213* | A simple graph is complete iff all vertices are connected by an edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐸)) | ||
Theorem | cusgredg 27214* | In a complete simple graph, the edges are all the pairs of different vertices. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ ComplUSGraph → 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | cplgr0 27215 | The null graph (with no vertices and no edges) represented by the empty set is a complete graph. (Contributed by AV, 1-Nov-2020.) |
⊢ ∅ ∈ ComplGraph | ||
Theorem | cusgr0 27216 | The null graph (with no vertices and no edges) represented by the empty set is a complete simple graph. (Contributed by AV, 1-Nov-2020.) |
⊢ ∅ ∈ ComplUSGraph | ||
Theorem | cplgr0v 27217 | A null graph (with no vertices) is a complete graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅) → 𝐺 ∈ ComplGraph) | ||
Theorem | cusgr0v 27218 | A graph with no vertices and no edges is a complete simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ ComplUSGraph) | ||
Theorem | cplgr1vlem 27219 | Lemma for cplgr1v 27220 and cusgr1v 27221. (Contributed by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((♯‘𝑉) = 1 → 𝐺 ∈ V) | ||
Theorem | cplgr1v 27220 | A graph with one vertex is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.) (Revised by AV, 1-Nov-2020.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((♯‘𝑉) = 1 → 𝐺 ∈ ComplGraph) | ||
Theorem | cusgr1v 27221 | A graph with one vertex and no edges is a complete simple graph. (Contributed by AV, 1-Nov-2020.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((♯‘𝑉) = 1 ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ ComplUSGraph) | ||
Theorem | cplgr2v 27222 | An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 2) → (𝐺 ∈ ComplGraph ↔ 𝑉 ∈ 𝐸)) | ||
Theorem | cplgr2vpr 27223 | An undirected hypergraph with two (different) vertices is complete iff there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.) (Revised by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (𝐺 ∈ UHGraph ∧ 𝑉 = {𝐴, 𝐵})) → (𝐺 ∈ ComplGraph ↔ {𝐴, 𝐵} ∈ 𝐸)) | ||
Theorem | nbcplgr 27224 | In a complete graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = (𝑉 ∖ {𝑁})) | ||
Theorem | cplgr3v 27225 | A pseudograph with three (different) vertices is complete iff there is an edge between each of these three vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ (Vtx‘𝐺) = {𝐴, 𝐵, 𝐶} ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝐺 ∈ UPGraph ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝐺 ∈ ComplGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))) | ||
Theorem | cusgr3vnbpr 27226* | The neighbors of a vertex in a simple graph with three elements are unordered pairs of the other vertices if and only if the graph is complete. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 5-Nov-2020.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ (Vtx‘𝐺) = {𝐴, 𝐵, 𝐶} & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝐺 ∈ USGraph ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝐺 ∈ ComplGraph ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(𝐺 NeighbVtx 𝑥) = {𝑦, 𝑧})) | ||
Theorem | cplgrop 27227 | A complete graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.) |
⊢ (𝐺 ∈ ComplGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ ComplGraph) | ||
Theorem | cusgrop 27228 | A complete simple graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ ComplUSGraph) | ||
Theorem | cusgrexilem1 27229* | Lemma 1 for cusgrexi 27233. (Contributed by Alexander van der Vekens, 12-Jan-2018.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V) | ||
Theorem | usgrexilem 27230* | Lemma for usgrexi 27231. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃):dom ( I ↾ 𝑃)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | usgrexi 27231* | An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 10-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈ USGraph) | ||
Theorem | cusgrexilem2 27232* | Lemma 2 for cusgrexi 27233. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒) | ||
Theorem | cusgrexi 27233* | An arbitrary set 𝑉 regarded as set of vertices together with the set of pairs of elements of this set regarded as edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.) (Proof shortened by AV, 14-Feb-2022.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈ ComplUSGraph) | ||
Theorem | cusgrexg 27234* | For each set there is a set of edges so that the set together with these edges is a complete simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 5-Nov-2020.) |
⊢ (𝑉 ∈ 𝑊 → ∃𝑒〈𝑉, 𝑒〉 ∈ ComplUSGraph) | ||
Theorem | structtousgr 27235* | Any (extensible) structure with a base set can be made a simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021.) (Revised by AV, 17-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 (Base‘𝑆) ∣ (♯‘𝑥) = 2} & ⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ 𝐺 = (𝑆 sSet 〈(.ef‘ndx), ( I ↾ 𝑃)〉) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑆) ⇒ ⊢ (𝜑 → 𝐺 ∈ USGraph) | ||
Theorem | structtocusgr 27236* | Any (extensible) structure with a base set can be made a complete simple graph with the set of pairs of elements of the base set regarded as edges. (Contributed by AV, 10-Nov-2021.) (Revised by AV, 17-Nov-2021.) (Proof shortened by AV, 14-Feb-2022.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 (Base‘𝑆) ∣ (♯‘𝑥) = 2} & ⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ 𝐺 = (𝑆 sSet 〈(.ef‘ndx), ( I ↾ 𝑃)〉) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑆) ⇒ ⊢ (𝜑 → 𝐺 ∈ ComplUSGraph) | ||
Theorem | cffldtocusgr 27237* | The field of complex numbers can be made a complete simple graph with the set of pairs of complex numbers regarded as edges. This theorem demonstrates the capabilities of the current definitions for graphs applied to extensible structures. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 17-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 ℂ ∣ (♯‘𝑥) = 2} & ⊢ 𝐺 = (ℂfld sSet 〈(.ef‘ndx), ( I ↾ 𝑃)〉) ⇒ ⊢ 𝐺 ∈ ComplUSGraph | ||
Theorem | cusgrres 27238* | Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ ComplUSGraph) | ||
Theorem | cusgrsizeindb0 27239 | Base case of the induction in cusgrsize 27244. The size of a complete simple graph with 0 vertices, actually of every null graph, is 0=((0-1)*0)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 0) → (♯‘𝐸) = ((♯‘𝑉)C2)) | ||
Theorem | cusgrsizeindb1 27240 | Base case of the induction in cusgrsize 27244. The size of a (complete) simple graph with 1 vertex is 0=((1-1)*1)/2. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 1) → (♯‘𝐸) = ((♯‘𝑉)C2)) | ||
Theorem | cusgrsizeindslem 27241* | Lemma for cusgrsizeinds 27242. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) = ((♯‘𝑉) − 1)) | ||
Theorem | cusgrsizeinds 27242* | Part 1 of induction step in cusgrsize 27244. The size of a complete simple graph with 𝑛 vertices is (𝑛 − 1) plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘𝐸) = (((♯‘𝑉) − 1) + (♯‘𝐹))) | ||
Theorem | cusgrsize2inds 27243* | Induction step in cusgrsize 27244. If the size of the complete graph with 𝑛 vertices reduced by one vertex is "(𝑛 − 1) choose 2", the size of the complete graph with 𝑛 vertices is "𝑛 choose 2". (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ (𝑌 ∈ ℕ0 → ((𝐺 ∈ ComplUSGraph ∧ (♯‘𝑉) = 𝑌 ∧ 𝑁 ∈ 𝑉) → ((♯‘𝐹) = ((♯‘(𝑉 ∖ {𝑁}))C2) → (♯‘𝐸) = ((♯‘𝑉)C2)))) | ||
Theorem | cusgrsize 27244 | The size of a finite complete simple graph with 𝑛 vertices (𝑛 ∈ ℕ0) is (𝑛C2) ("𝑛 choose 2") resp. (((𝑛 − 1)∗𝑛) / 2), see definition in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 10-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin) → (♯‘𝐸) = ((♯‘𝑉)C2)) | ||
Theorem | cusgrfilem1 27245* | Lemma 1 for cusgrfi 27248. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑃 ⊆ (Edg‘𝐺)) | ||
Theorem | cusgrfilem2 27246* | Lemma 2 for cusgrfi 27248. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃) | ||
Theorem | cusgrfilem3 27247* | Lemma 3 for cusgrfi 27248. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin)) | ||
Theorem | cusgrfi 27248 | If the size of a complete simple graph is finite, then its order is also finite. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝐸 ∈ Fin) → 𝑉 ∈ Fin) | ||
Theorem | usgredgsscusgredg 27249 | A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → 𝐸 ⊆ 𝐹) | ||
Theorem | usgrsscusgr 27250* | A simple graph is a subgraph of a complete simple graph. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → ∀𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 𝑒 = 𝑓) | ||
Theorem | sizusglecusglem1 27251 | Lemma 1 for sizusglecusg 27253. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → ( I ↾ 𝐸):𝐸–1-1→𝐹) | ||
Theorem | sizusglecusglem2 27252 | Lemma 2 for sizusglecusg 27253. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph ∧ 𝐹 ∈ Fin) → 𝐸 ∈ Fin) | ||
Theorem | sizusglecusg 27253 | The size of a simple graph with 𝑛 vertices is at most the size of a complete simple graph with 𝑛 vertices (𝑛 may be infinite). (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 13-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐻) & ⊢ 𝐹 = (Edg‘𝐻) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) → (♯‘𝐸) ≤ (♯‘𝐹)) | ||
Theorem | fusgrmaxsize 27254 | The maximum size of a finite simple graph with 𝑛 vertices is (((𝑛 − 1)∗𝑛) / 2). See statement in section I.1 of [Bollobas] p. 3 . (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 14-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (♯‘𝐸) ≤ ((♯‘𝑉)C2)) | ||
Syntax | cvtxdg 27255 | Extend class notation with the vertex degree function. |
class VtxDeg | ||
Definition | df-vtxdg 27256* | Define the vertex degree function for a graph. To be appropriate for arbitrary hypergraphs, we have to double-count those edges that contain 𝑢 "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +𝑒 is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.) |
⊢ VtxDeg = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(iEdg‘𝑔) / 𝑒⦌(𝑢 ∈ 𝑣 ↦ ((♯‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))) | ||
Theorem | vtxdgfval 27257* | The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 9-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = (𝑢 ∈ 𝑉 ↦ ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐼‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑢}})))) | ||
Theorem | vtxdgval 27258* | The degree of a vertex. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) +𝑒 (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}}))) | ||
Theorem | vtxdgfival 27259* | The degree of a vertex for graphs of finite size. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 8-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)}) + (♯‘{𝑥 ∈ 𝐴 ∣ (𝐼‘𝑥) = {𝑈}}))) | ||
Theorem | vtxdgop 27260 | The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.) |
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) | ||
Theorem | vtxdgf 27261 | The vertex degree function is a function from vertices to extended nonnegative integers. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 10-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺):𝑉⟶ℕ0*) | ||
Theorem | vtxdgelxnn0 27262 | The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑋) ∈ ℕ0*) | ||
Theorem | vtxdg0v 27263 | The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 = ∅ ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = 0) | ||
Theorem | vtxdg0e 27264 | The degree of a vertex in an empty graph is zero, because there are no edges. This is the base case for the induction for calculating the degree of a vertex, for example in a Königsberg graph (see also the induction steps vdegp1ai 27326, vdegp1bi 27327 and vdegp1ci 27328). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝑈 ∈ 𝑉 ∧ 𝐼 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0) | ||
Theorem | vtxdgfisnn0 27265 | The degree of a vertex in a graph of finite size is a nonnegative integer. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 11-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) ∈ ℕ0) | ||
Theorem | vtxdgfisf 27266 | The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐴 ∈ Fin) → (VtxDeg‘𝐺):𝑉⟶ℕ0) | ||
Theorem | vtxdeqd 27267 | Equality theorem for the vertex degree: If two graphs are structurally equal, their vertex degree functions are equal. (Contributed by AV, 26-Feb-2021.) |
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐻 ∈ 𝑌) & ⊢ (𝜑 → (Vtx‘𝐻) = (Vtx‘𝐺)) & ⊢ (𝜑 → (iEdg‘𝐻) = (iEdg‘𝐺)) ⇒ ⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺)) | ||
Theorem | vtxduhgr0e 27268 | The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 27264. (Contributed by AV, 15-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0) | ||
Theorem | vtxdlfuhgr1v 27269* | The degree of the vertex in a loop-free hypergraph with one vertex is 0. (Contributed by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 1 ∧ 𝐼:dom 𝐼⟶𝐸) → (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = 0)) | ||
Theorem | vdumgr0 27270 | A vertex in a multigraph has degree 0 if the graph consists of only one vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 2-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ∧ (♯‘𝑉) = 1) → ((VtxDeg‘𝐺)‘𝑁) = 0) | ||
Theorem | vtxdun 27271 | The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 19-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → Fun 𝐽) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁))) | ||
Theorem | vtxdfiun 27272 | The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 19-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → Fun 𝐽) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) & ⊢ (𝜑 → dom 𝐼 ∈ Fin) & ⊢ (𝜑 → dom 𝐽 ∈ Fin) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁))) | ||
Theorem | vtxduhgrun 27273 | The degree of a vertex in the union of two hypergraphs on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) +𝑒 ((VtxDeg‘𝐻)‘𝑁))) | ||
Theorem | vtxduhgrfiun 27274 | The degree of a vertex in the union of two hypergraphs of finite size on the same vertex set is the sum of the degrees of the vertex in each hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.) (Revised by AV, 7-Dec-2020.) (Proof shortened by AV, 19-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐽 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (dom 𝐼 ∩ dom 𝐽) = ∅) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐼 ∪ 𝐽)) & ⊢ (𝜑 → dom 𝐼 ∈ Fin) & ⊢ (𝜑 → dom 𝐽 ∈ Fin) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑈)‘𝑁) = (((VtxDeg‘𝐺)‘𝑁) + ((VtxDeg‘𝐻)‘𝑁))) | ||
Theorem | vtxdlfgrval 27275* | The value of the vertex degree function for a loop-free graph 𝐺. (Contributed by AV, 23-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐼:𝐴⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)})) | ||
Theorem | vtxdumgrval 27276* | The value of the vertex degree function for a multigraph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 23-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)})) | ||
Theorem | vtxdusgrval 27277* | The value of the vertex degree function for a simple graph. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 11-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐴 = dom 𝐼 & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐼‘𝑥)})) | ||
Theorem | vtxd0nedgb 27278* | A vertex has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ (𝑈 ∈ 𝑉 → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) | ||
Theorem | vtxdushgrfvedglem 27279* | Lemma for vtxdushgrfvedg 27280 and vtxdusgrfvedg 27281. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (♯‘{𝑖 ∈ dom (iEdg‘𝐺) ∣ 𝑈 ∈ ((iEdg‘𝐺)‘𝑖)}) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | vtxdushgrfvedg 27280* | The value of the vertex degree function for a simple hypergraph. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = ((♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}) +𝑒 (♯‘{𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑈}}))) | ||
Theorem | vtxdusgrfvedg 27281* | The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | vtxduhgr0nedg 27282* | If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ (𝐷‘𝑈) = 0) → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸) | ||
Theorem | vtxdumgr0nedg 27283* | If a vertex in a multigraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by AV, 12-Dec-2020.) (Proof shortened by AV, 15-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑈 ∈ 𝑉 ∧ (𝐷‘𝑈) = 0) → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸) | ||
Theorem | vtxduhgr0edgnel 27284* | A vertex in a hypergraph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 24-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||
Theorem | vtxdusgr0edgnel 27285* | A vertex in a simple graph has degree 0 iff there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||
Theorem | vtxdusgr0edgnelALT 27286* | Alternate proof of vtxdusgr0edgnel 27285, not based on vtxduhgr0edgnel 27284. A vertex in a simple graph has degree 0 if there is no edge incident with this vertex. (Contributed by AV, 17-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒)) | ||
Theorem | vtxdgfusgrf 27287 | The vertex degree function on finite simple graphs is a function from vertices to nonnegative integers. (Contributed by AV, 12-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (VtxDeg‘𝐺):𝑉⟶ℕ0) | ||
Theorem | vtxdgfusgr 27288* | In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 12-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ∈ ℕ0) | ||
Theorem | fusgrn0degnn0 27289* | In a nonempty, finite graph there is a vertex having a nonnegative integer as degree. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Revised by AV, 1-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → ∃𝑣 ∈ 𝑉 ∃𝑛 ∈ ℕ0 ((VtxDeg‘𝐺)‘𝑣) = 𝑛) | ||
Theorem | 1loopgruspgr 27290 | A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 27039). (Contributed by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → 𝐺 ∈ USPGraph) | ||
Theorem | 1loopgredg 27291 | The set of edges in a graph (simple pseudograph) with one edge which is a loop is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → (Edg‘𝐺) = {{𝑁}}) | ||
Theorem | 1loopgrnb0 27292 | In a graph (simple pseudograph) with one edge which is a loop, the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → (𝐺 NeighbVtx 𝑁) = ∅) | ||
Theorem | 1loopgrvd2 27293 | 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, 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, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝑁) = 2) | ||
Theorem | 1loopgrvd0 27294 | The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) & ⊢ (𝜑 → 𝐾 ∈ (𝑉 ∖ {𝑁})) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐾) = 0) | ||
Theorem | 1hevtxdg0 27295 | 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 27296 | 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 27297 | 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 27298 | 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 27299 | 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 27300 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |