Home | Metamath
Proof Explorer Theorem List (p. 264 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 | uvtxnbgr 26301 | A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → (𝐺 NeighbVtx 𝑁) = (𝑉 ∖ {𝑁})) | ||
Theorem | uvtxnbgrb 26302 | A vertex is universal iff all the other vertices are its neighbors. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝐺 NeighbVtx 𝑁) = (𝑉 ∖ {𝑁}))) | ||
Theorem | uvtxusgr 26303* | The set of all universal vertices of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 31-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (UnivVtx‘𝐺) = {𝑛 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑛}){𝑘, 𝑛} ∈ 𝐸}) | ||
Theorem | uvtxusgrel 26304* | A universal vertex, i.e. an element of the set of all universal vertices, of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 31-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁}){𝑘, 𝑁} ∈ 𝐸))) | ||
Theorem | uvtxanm1nbgr 26305 | A universal vertex has 𝑛 − 1 neighbors in a finite graph with 𝑛 vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ (UnivVtx‘𝐺)) → (#‘(𝐺 NeighbVtx 𝑁)) = ((#‘𝑉) − 1)) | ||
Theorem | nbusgrvtxm1uvtx 26306 | If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, the vertex is universal. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → 𝑈 ∈ (UnivVtx‘𝐺))) | ||
Theorem | uvtxnbvtxm1 26307 | A universal vertex has 𝑛 − 1 neighbors in a finite simple graph with 𝑛 vertices. A biconditional version of nbusgrvtxm1uvtx 26306 resp. uvtxanm1nbgr 26305. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (𝑈 ∈ (UnivVtx‘𝐺) ↔ (#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1))) | ||
Theorem | nbupgruvtxres 26308* | The neighborhood of a universal vertex in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾}))) | ||
Theorem | uvtxupgrres 26309* | A universal vertex is universal in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → (𝐾 ∈ (UnivVtx‘𝐺) → 𝐾 ∈ (UnivVtx‘𝑆))) | ||
Theorem | iscplgr 26310* | The property of being a complete graph. (Contributed by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))) | ||
Theorem | cplgruvtxb 26311 | An graph is complete iff each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ (UnivVtx‘𝐺) = 𝑉)) | ||
Theorem | iscplgrnb 26312* | A graph is complete iff all vertices are neighbors of all vertices. (Contributed by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ComplGraph ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))) | ||
Theorem | iscplgredg 26313* | 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 26314 | The property of being a complete simple graph. (Contributed by AV, 1-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph)) | ||
Theorem | cusgrusgr 26315 | 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 26316 | A complete simple graph is a complete graph. (Contributed by AV, 1-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph → 𝐺 ∈ ComplGraph) | ||
Theorem | iscusgrvtx 26317* | A simple graph is complete iff all vertices are uniuversal. (Contributed by AV, 1-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ ComplUSGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))) | ||
Theorem | cusgruvtxb 26318 | 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 26319* | 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 26320* | 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 26321 | 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 26322 | 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 26323 | 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 26324 | 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 26325 | Lemma for cplgr1v 26326 and cusgr1v 26327. (Contributed by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((#‘𝑉) = 1 → 𝐺 ∈ V) | ||
Theorem | cplgr1v 26326 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((#‘𝑉) = 1 → 𝐺 ∈ ComplGraph) | ||
Theorem | cusgr1v 26327 | 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 26328 | 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 26329 | 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 26330 | 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 26331 | 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.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ (Vtx‘𝐺) = {𝐴, 𝐵, 𝐶} ⇒ ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ 𝐺 ∈ UPGraph ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (𝐺 ∈ ComplGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))) | ||
Theorem | cusgr3vnbpr 26332* | 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 26333 | A complete graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.) |
⊢ (𝐺 ∈ ComplGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ ComplGraph) | ||
Theorem | cusgrop 26334 | A complete simple graph represented by an ordered pair. (Contributed by AV, 10-Nov-2020.) |
⊢ (𝐺 ∈ ComplUSGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ ComplUSGraph) | ||
Theorem | cusgrexilem1 26335* | Lemma 1 for cusgrexi 26339. (Contributed by Alexander van der Vekens, 12-Jan-2018.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃) ∈ V) | ||
Theorem | usgrexilem 26336* | Lemma for usgrexi 26337. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → ( I ↾ 𝑃):dom ( I ↾ 𝑃)–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) | ||
Theorem | usgrexi 26337* | 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 26338* | Lemma 2 for cusgrexi 26339. (Contributed by AV, 12-Jan-2018.) (Revised by AV, 10-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ⇒ ⊢ (((𝑉 ∈ 𝑊 ∧ 𝑣 ∈ 𝑉) ∧ 𝑛 ∈ (𝑉 ∖ {𝑣})) → ∃𝑒 ∈ ran ( I ↾ 𝑃){𝑣, 𝑛} ⊆ 𝑒) | ||
Theorem | cusgrexi 26339* | An arbitrary set regarded as 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, 10-Nov-2021.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ⇒ ⊢ (𝑉 ∈ 𝑊 → 〈𝑉, ( I ↾ 𝑃)〉 ∈ ComplUSGraph) | ||
Theorem | cusgrexg 26340* | 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 26341* | 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 26342* | 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.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 (Base‘𝑆) ∣ (#‘𝑥) = 2} & ⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ 𝐺 = (𝑆 sSet 〈(.ef‘ndx), ( I ↾ 𝑃)〉) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑆) ⇒ ⊢ (𝜑 → 𝐺 ∈ ComplUSGraph) | ||
Theorem | cffldtocusgr 26343* | 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 26344* | Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ ComplUSGraph) | ||
Theorem | cusgrsizeindb0 26345 | Base case of the induction in cusgrsize 26350. 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 26346 | Base case of the induction in cusgrsize 26350. 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 26347* | Lemma for cusgrsizeinds 26348. (Contributed by Alexander van der Vekens, 11-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉) → (#‘{𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒}) = ((#‘𝑉) − 1)) | ||
Theorem | cusgrsizeinds 26348* | Part 1 of induction step in cusgrsize 26350. 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 26349* | Induction step in cusgrsize 26350. 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 26350 | 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 26351* | Lemma 1 for cusgrfi 26354. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} ⇒ ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉) → 𝑃 ⊆ (Edg‘𝐺)) | ||
Theorem | cusgrfilem2 26352* | Lemma 2 for cusgrfi 26354. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐹:(𝑉 ∖ {𝑁})–1-1-onto→𝑃) | ||
Theorem | cusgrfilem3 26353* | Lemma 3 for cusgrfi 26354. (Contributed by Alexander van der Vekens, 13-Jan-2018.) (Revised by AV, 11-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 (𝑎 ≠ 𝑁 ∧ 𝑥 = {𝑎, 𝑁})} & ⊢ 𝐹 = (𝑥 ∈ (𝑉 ∖ {𝑁}) ↦ {𝑥, 𝑁}) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑉 ∈ Fin ↔ 𝑃 ∈ Fin)) | ||
Theorem | cusgrfi 26354 | 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 26355 | 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 26356* | 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 26357 | Lemma 1 for sizusglecusg 26359. (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 26358 | Lemma 2 for sizusglecusg 26359. (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 26359 | 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 26360 | 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 26361 | Extend class notation with the vertex degree function. |
class VtxDeg | ||
Definition | df-vtxdg 26362* | 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 26363* | 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 26364* | 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 26365* | 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 26366 | The vertex degree expressed as operation. (Contributed by AV, 12-Dec-2021.) |
⊢ (𝐺 ∈ 𝑊 → (VtxDeg‘𝐺) = ((Vtx‘𝐺)VtxDeg(iEdg‘𝐺))) | ||
Theorem | vtxdgf 26367 | 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 26368 | 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 26369 | 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 26370 | 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 26432, vdegp1bi 26433 and vdegp1ci 26434). (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 26371 | 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 26372 | 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 26373 | 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 26374 | The degree of a vertex in an empty hypergraph is zero, because there are no edges. Analogue of vtxdg0e 26370. (Contributed by AV, 15-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 = ∅) → ((VtxDeg‘𝐺)‘𝑈) = 0) | ||
Theorem | vtxdlfuhgr1v 26375* | 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 26376 | 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 26377 | 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 26378 | 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 26379 | 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 26380 | 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 26381* | 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 26382* | 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 26383* | 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 26384* | 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 26385* | Lemma for vtxdushgrfvedg 26386 and vtxdusgrfvedg 26387. (Contributed by AV, 12-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USHGraph ∧ 𝑈 ∈ 𝑉) → (#‘{𝑖 ∈ dom (iEdg‘𝐺) ∣ 𝑈 ∈ ((iEdg‘𝐺)‘𝑖)}) = (#‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | vtxdushgrfvedg 26386* | 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 26387* | The value of the vertex degree function for a simple graph. (Contributed by AV, 12-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐷 = (VtxDeg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (𝐷‘𝑈) = (#‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | vtxduhgr0nedg 26388* | 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 26389* | 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 26390* | 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 26391* | 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 26392* | Alternate proof of vtxdusgr0edgnel 26391, not based on vtxduhgr0edgnel 26390. 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 26393 | 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 26394* | 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 26395* | 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 26396 | A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop 26141). (Contributed by AV, 21-Feb-2021.) |
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝑁}〉}) ⇒ ⊢ (𝜑 → 𝐺 ∈ USPGraph ) | ||
Theorem | 1loopgredg 26397 | 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 26398 | 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 26399 | 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 26400 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |