Home | Metamath
Proof Explorer Theorem List (p. 273 of 450) | < 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-28698) |
Hilbert Space Explorer
(28699-30221) |
Users' Mathboxes
(30222-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iscplgrnb 27201* | A graph is complete iff all vertices are neighbors of all vertices. (Contributed by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))) | ||
Theorem | iscplgredg 27202* | 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 27203 | The property of being a complete simple graph. (Contributed by AV, 1-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph)) | ||
Theorem | cusgrusgr 27204 | 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 27205 | A complete simple graph is a complete graph. (Contributed by AV, 1-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph → 𝐺 ∈ ComplGraph) | ||
Theorem | iscusgrvtx 27206* | A simple graph is complete iff all vertices are uniuversal. (Contributed by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))) | ||
Theorem | cusgruvtxb 27207 | 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 27208* | 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 27209* | 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 27210 | 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 27211 | 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 27212 | 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 27213 | 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 27214 | Lemma for cplgr1v 27215 and cusgr1v 27216. (Contributed by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((♯‘𝑉) = 1 → 𝐺 ∈ V) | ||
Theorem | cplgr1v 27215 | 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 27216 | 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 27217 | 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 27218 | 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 27219 | 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 27220 | 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 27221* | 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 27222 | A complete graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.) |
⊢ (𝐺 ∈ ComplGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ ComplGraph) | ||
Theorem | cusgrop 27223 | A complete simple graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ ComplUSGraph) | ||
Theorem | cusgrexilem1 27224* | Lemma 1 for cusgrexi 27228. (Contributed by Alexander van der Vekens, 12-Jan-2018.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V) | ||
Theorem | usgrexilem 27225* | Lemma for usgrexi 27226. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃):dom ( I ↾ 𝑃)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) | ||
Theorem | usgrexi 27226* | 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 27227* | Lemma 2 for cusgrexi 27228. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒) | ||
Theorem | cusgrexi 27228* | 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 27229* | 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 27230* | 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 27231* | 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 27232* | 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 27233* | Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ ComplUSGraph) | ||
Theorem | cusgrsizeindb0 27234 | Base case of the induction in cusgrsize 27239. 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 27235 | Base case of the induction in cusgrsize 27239. 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 27236* | Lemma for cusgrsizeinds 27237. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (♯‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) = ((♯‘𝑉) − 1)) | ||
Theorem | cusgrsizeinds 27237* | Part 1 of induction step in cusgrsize 27239. 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 27238* | Induction step in cusgrsize 27239. 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 27239 | 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 27240* | Lemma 1 for cusgrfi 27243. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑃 ⊆ (Edg‘𝐺)) | ||
Theorem | cusgrfilem2 27241* | Lemma 2 for cusgrfi 27243. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃) | ||
Theorem | cusgrfilem3 27242* | Lemma 3 for cusgrfi 27243. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin)) | ||
Theorem | cusgrfi 27243 | 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 27244 | 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 27245* | 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 27246 | Lemma 1 for sizusglecusg 27248. (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 27247 | Lemma 2 for sizusglecusg 27248. (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 27248 | 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 27249 | 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 27250 | Extend class notation with the vertex degree function. |
class VtxDeg | ||
Definition | df-vtxdg 27251* | 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 27252* | 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 27253* | 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 27254* | 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 27255 | The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.) |
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) | ||
Theorem | vtxdgf 27256 | 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 27257 | 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 27258 | 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 27259 | 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 27321, vdegp1bi 27322 and vdegp1ci 27323). (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 27260 | 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 27261 | 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 27262 | 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 27263 | The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 27259. (Contributed by AV, 15-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0) | ||
Theorem | vtxdlfuhgr1v 27264* | 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 27265 | 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 27266 | 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 27267 | 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 27268 | 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 27269 | 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 27270* | 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 27271* | 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 27272* | 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 27273* | 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 27274* | Lemma for vtxdushgrfvedg 27275 and vtxdusgrfvedg 27276. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (♯‘{𝑖 ∈ dom (iEdg‘𝐺) ∣ 𝑈 ∈ ((iEdg‘𝐺)‘𝑖)}) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | vtxdushgrfvedg 27275* | 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 27276* | The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (♯‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | vtxduhgr0nedg 27277* | 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 27278* | 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 27279* | 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 27280* | 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 27281* | Alternate proof of vtxdusgr0edgnel 27280, not based on vtxduhgr0edgnel 27279. 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 27282 | 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 27283* | 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 27284* | 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 27285 | A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 27034). (Contributed by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → 𝐺 ∈ USPGraph) | ||
Theorem | 1loopgredg 27286 | 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 27287 | 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 27288 | 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 27289 | 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 27290 | 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 27291 | 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 27292 | 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 27293 | 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 27294 | 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 27295 | 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 27296 | 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 27297 | Lemma for p1evtxdeq 27298 and p1evtxdp1 27299. (Contributed by AV, 3-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {〈𝐾, 𝐸〉})) & ⊢ (𝜑 → 𝐾 ∈ 𝑋) & ⊢ (𝜑 → 𝐾 ∉ dom 𝐼) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 ((VtxDeg‘〈𝑉, {〈𝐾, 𝐸〉}〉)‘𝑈))) | ||
Theorem | p1evtxdeq 27298 | 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 27299 | 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 27300 | The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 27034). (Contributed by AV, 17-Dec-2020.) |
⊢ 𝐺 = 〈𝑉, {〈𝐴, {𝑁}〉}〉 ⇒ ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |