Home | Metamath
Proof Explorer Theorem List (p. 263 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 | upgrres1lem1 26201* | Lemma 1 for upgrres1 26205. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝑉 ∖ {𝑁}) ∈ V ∧ ( I ↾ 𝐹) ∈ V) | ||
Theorem | umgrres1lem 26202* | Lemma for umgrres1 26206. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ran ( I ↾ 𝐹) ⊆ {𝑝 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (#‘𝑝) = 2}) | ||
Theorem | upgrres1lem2 26203* | Lemma 2 for upgrres1 26205. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁}) | ||
Theorem | upgrres1lem3 26204* | Lemma 3 for upgrres1 26205. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (iEdg‘𝑆) = ( I ↾ 𝐹) | ||
Theorem | upgrres1 26205* | A pseudograph obtained by removing one vertex and all edges incident with this vertex is a pseudograph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr 26160 since the domains of the edge functions may not be compatible. (Contributed by AV, 8-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph ) | ||
Theorem | umgrres1 26206* | A multigraph obtained by removing one vertex and all edges incident with this vertex is a multigraph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr 26160 since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph ) | ||
Theorem | usgrres1 26207* | Restricting a simple graph by removing one vertex results in a simple graph. Remark: This restricted graph is not a subgraph of the original graph in the sense of df-subgr 26160 since the domains of the edge functions may not be compatible. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 10-Jan-2020.) (Revised by AV, 23-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ USGraph ) | ||
Syntax | cfusgr 26208 | Extend class notation with finite simple graphs. |
class FinUSGraph | ||
Definition | df-fusgr 26209 | Define the class of all finite undirected simple graphs without loops (called "finite simple graphs" in the following). A finite simple graph is an undirected simple graph of finite order, i.e. with a finite set of vertices. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
⊢ FinUSGraph = {𝑔 ∈ USGraph ∣ (Vtx‘𝑔) ∈ Fin} | ||
Theorem | isfusgr 26210 | The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ 𝑉 ∈ Fin)) | ||
Theorem | fusgrvtxfi 26211 | A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) | ||
Theorem | isfusgrf1 26212* | The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ FinUSGraph ↔ (𝐼:dom 𝐼–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} ∧ 𝑉 ∈ Fin))) | ||
Theorem | isfusgrcl 26213 | The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020.) (Revised by AV, 9-Jan-2020.) |
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧ (#‘(Vtx‘𝐺)) ∈ ℕ0)) | ||
Theorem | fusgrusgr 26214 | A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph ) | ||
Theorem | opfusgr 26215 | A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (〈𝑉, 𝐸〉 ∈ FinUSGraph ↔ (〈𝑉, 𝐸〉 ∈ USGraph ∧ 𝑉 ∈ Fin))) | ||
Theorem | usgredgffibi 26216 | The number of edges in a simple graph is finite iff its edge function is finite. (Contributed by AV, 10-Jan-2020.) (Revised by AV, 22-Oct-2020.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (𝐸 ∈ Fin ↔ 𝐼 ∈ Fin)) | ||
Theorem | fusgredgfi 26217* | In a finite simple graph the number of edges which contain a given vertex is also finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 21-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒} ∈ Fin) | ||
Theorem | usgr1v0e 26218 | The size of a (finite) simple graph with 1 vertex is 0. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 22-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ (#‘𝑉) = 1) → (#‘𝐸) = 0) | ||
Theorem | usgrfilem 26219* | In a finite simple graph, the number of edges is finite iff the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018.) (Revised by AV, 9-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝐸 ∈ Fin ↔ 𝐹 ∈ Fin)) | ||
Theorem | fusgrfisbase 26220 | Induction base for fusgrfis 26222. Main work is done in uhgr0v0e 26130. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 〈𝑉, 𝐸〉 ∈ USGraph ∧ (#‘𝑉) = 0) → 𝐸 ∈ Fin) | ||
Theorem | fusgrfisstep 26221* | Induction step in fusgrfis 26222: In a finite simple graph, the number of edges is finite if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 〈𝑉, 𝐸〉 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (( I ↾ {𝑝 ∈ (Edg‘〈𝑉, 𝐸〉) ∣ 𝑁 ∉ 𝑝}) ∈ Fin → 𝐸 ∈ Fin)) | ||
Theorem | fusgrfis 26222 | A finite simple graph is of finite size, i.e. has a finite number of edges. (Contributed by Alexander van der Vekens, 6-Jan-2018.) (Revised by AV, 8-Nov-2020.) |
⊢ (𝐺 ∈ FinUSGraph → (Edg‘𝐺) ∈ Fin) | ||
Theorem | fusgrfupgrfs 26223 | A finite simple graph is a finite pseudograph of finite size. (Contributed by AV, 27-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → (𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin)) | ||
Syntax | cnbgr 26224 | Extend class notation with neighbors (of a vertex in a graph). |
class NeighbVtx | ||
Syntax | cuvtxa 26225 | Extend class notation with the universal vertices (in a graph). |
class UnivVtx | ||
Syntax | ccplgr 26226 | Extend class notation with (arbitrary) complete graphs. |
class ComplGraph | ||
Syntax | ccusgr 26227 | Extend class notation with complete simple graphs. |
class ComplUSGraph | ||
Definition | df-nbgr 26228* |
Define the (open) neighborhood resp. the class of all neighbors of a
vertex (in a graph), see definition in section I.1 of [Bollobas] p. 3 or
definition in section 1.1 of [Diestel]
p. 3. The neighborhood/neighbors
of a vertex are all (other) vertices which are connected with this
vertex by an edge. In contrast to a closed neighborhood, a vertex is
not a neighbor of itself. This definition is applicable even for
arbitrary hypergraphs.
Remark: To distinguish this definition from other definitions for neighborhoods resp. neighbors (e.g., nei in Topology, see df-nei 20902), the suffix Vtx is added to the class constant NeighbVtx. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.) |
⊢ NeighbVtx = (𝑔 ∈ V, 𝑣 ∈ (Vtx‘𝑔) ↦ {𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣}) ∣ ∃𝑒 ∈ (Edg‘𝑔){𝑣, 𝑛} ⊆ 𝑒}) | ||
Theorem | nbgrprc0 26229 | The set of neighbors is empty if the graph or the vertex are proper classes. (Contributed by AV, 26-Oct-2020.) |
⊢ (¬ (𝐺 ∈ V ∧ 𝑁 ∈ V) → (𝐺 NeighbVtx 𝑁) = ∅) | ||
Definition | df-uvtxa 26230* | Define the class of all universal vertices (in graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph) resp. all other vertices are its neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.) |
⊢ UnivVtx = (𝑔 ∈ V ↦ {𝑣 ∈ (Vtx‘𝑔) ∣ ∀𝑛 ∈ ((Vtx‘𝑔) ∖ {𝑣})𝑛 ∈ (𝑔 NeighbVtx 𝑣)}) | ||
Definition | df-cplgr 26231* | 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. (Contributed by AV, 24-Oct-2020.) |
⊢ ComplGraph = {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)𝑣 ∈ (UnivVtx‘𝑔)} | ||
Definition | df-cusgr 26232 | 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 26350. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 24-Oct-2020.) |
⊢ ComplUSGraph = {𝑔 ∈ USGraph ∣ 𝑔 ∈ ComplGraph} | ||
Theorem | nbgrcl 26233 | If a class has at least one neighbor, it must be a vertex. (Contributed by AV, 6-Jun-2021.) |
⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝑋) → 𝑋 ∈ (Vtx‘𝐺)) | ||
Theorem | nbgrval 26234* | The set of neighbors of a vertex 𝑉 in a graph 𝐺. (Contributed by Alexander van der Vekens, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) | ||
Theorem | dfnbgr2 26235* | Alternate definition of the neighbors of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 15-Nov-2020.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 (𝑁 ∈ 𝑒 ∧ 𝑛 ∈ 𝑒)}) | ||
Theorem | dfnbgr3 26236* | Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval 26234). (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 25-Oct-2020.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ Fun 𝐼) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑖 ∈ dom 𝐼{𝑁, 𝑛} ⊆ (𝐼‘𝑖)}) | ||
Theorem | nbgrnvtx0 26237 | There are no neighbors of a class which is not a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∉ 𝑉 → (𝐺 NeighbVtx 𝑁) = ∅) | ||
Theorem | nbgrel 26238* | Characterization of a neighbor of a vertex 𝑉 in a graph 𝐺. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 6-Jun-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐾 ∈ (𝐺 NeighbVtx 𝑁) ↔ ((𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ≠ 𝑁 ∧ ∃𝑒 ∈ 𝐸 {𝑁, 𝐾} ⊆ 𝑒))) | ||
Theorem | nbuhgr 26239* | The set of neighbors of a vertex in a hypergraph. This version of nbgrval 26234 (with 𝑁 being an arbitrary set instead of being a vertex) only holds for classes whose edges are subsets of the set of vertices (hypergraphs!). (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 15-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑋) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ ∃𝑒 ∈ 𝐸 {𝑁, 𝑛} ⊆ 𝑒}) | ||
Theorem | nbupgr 26240* | The set of neighbors of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.) (Proof shortened by AV, 30-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ (𝑉 ∖ {𝑁}) ∣ {𝑁, 𝑛} ∈ 𝐸}) | ||
Theorem | nbupgrel 26241 | A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾)) → (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑁, 𝐾} ∈ 𝐸)) | ||
Theorem | nbumgrvtx 26242* | The set of neighbors of a vertex in a multigraph. (Contributed by AV, 27-Nov-2020.) (Proof shortened by AV, 30-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) | ||
Theorem | nbumgr 26243* | The set of neighbors of an arbitrary class in a multigraph. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) | ||
Theorem | nbusgrvtx 26244* | The set of neighbors of a vertex in a simple graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) | ||
Theorem | nbusgr 26245* | The set of neighbors of an arbitrary class in a simple graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) | ||
Theorem | nbgr2vtx1edg 26246* | If a graph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020.) (Revised by AV, 25-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((#‘𝑉) = 2 ∧ 𝑉 ∈ 𝐸) → ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)) | ||
Theorem | nbuhgr2vtx1edgblem 26247* | Lemma for nbuhgr2vtx1edgb 26248. This reverse direction of nbgr2vtx1edg 26246 only holds for classes whose edges are subsets of the set of vertices (hypergraphs!) (Contributed by AV, 2-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏} ∧ 𝑎 ∈ (𝐺 NeighbVtx 𝑏)) → {𝑎, 𝑏} ∈ 𝐸) | ||
Theorem | nbuhgr2vtx1edgb 26248* | If a hypergraph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 2) → (𝑉 ∈ 𝐸 ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))) | ||
Theorem | nbusgreledg 26249 | A class/vertex is a neighbor of another class/vertex in a simple graph iff the vertices are endpoints of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017.) (Revised by AV, 26-Oct-2020.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑁, 𝐾} ∈ 𝐸)) | ||
Theorem | uhgrnbgr0nb 26250* | A vertex which is not endpoint of an edge has no neighbor in a hypergraph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ ∀𝑒 ∈ (Edg‘𝐺)𝑁 ∉ 𝑒) → (𝐺 NeighbVtx 𝑁) = ∅) | ||
Theorem | nbgr0vtxlem 26251* | Lemma for nbgr0vtx 26252 and nbgr0edg 26253. (Contributed by AV, 15-Nov-2020.) |
⊢ (𝜑 → ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝐾}) ¬ ∃𝑒 ∈ (Edg‘𝐺){𝐾, 𝑛} ⊆ 𝑒) ⇒ ⊢ (𝜑 → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr0vtx 26252 | In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr0edg 26253 | In an empty graph (with no edges), every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Proof shortened by AV, 15-Nov-2020.) |
⊢ ((Edg‘𝐺) = ∅ → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr1vtx 26254 | In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
⊢ ((#‘(Vtx‘𝐺)) = 1 → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgrisvtx 26255 | Every neighbor of a class/vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑁 ∈ (𝐺 NeighbVtx 𝐾)) → 𝑁 ∈ 𝑉) | ||
Theorem | nbgrssvtx 26256 | The neighbors of a vertex in a graph are a subset of all vertices of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 NeighbVtx 𝑁) ⊆ 𝑉) | ||
Theorem | nbgrnself 26257* | A vertex in a graph is not a neighbor of itself. (Contributed by by AV, 3-Nov-2020.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ∀𝑣 ∈ 𝑉 𝑣 ∉ (𝐺 NeighbVtx 𝑣) | ||
Theorem | usgrnbnself 26258* | A vertex in a simple graph is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 27-Oct-2020.) (Proof shortened by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → ∀𝑣 ∈ 𝑉 𝑣 ∉ (𝐺 NeighbVtx 𝑣)) | ||
Theorem | nbgrnself2 26259 | A class is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.) |
⊢ (𝐺 ∈ 𝑊 → 𝑁 ∉ (𝐺 NeighbVtx 𝑁)) | ||
Theorem | nbgrssovtx 26260 | The neighbors of a vertex are a subset of all vertices except the vertex itself. Stronger version of nbgrssvtx 26256. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 NeighbVtx 𝑁) ⊆ (𝑉 ∖ {𝑁})) | ||
Theorem | nbgrssvwo2 26261 | The neighbors of a vertex are a subset of all vertices except the vertex itself and a vertex which is not a neighbor. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑀 ∉ (𝐺 NeighbVtx 𝑁)) → (𝐺 NeighbVtx 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁})) | ||
Theorem | usgrnbnself2 26262 | In a simple graph, a class is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 27-Oct-2020.) (Proof shortened by AV, 3-Nov-2020.) |
⊢ (𝐺 ∈ USGraph → 𝑁 ∉ (𝐺 NeighbVtx 𝑁)) | ||
Theorem | usgrnbssovtx 26263 | The neighbors of a vertex in a simple graph are a subset of all vertices of the graph except the vertex itself. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 27-Oct-2020.) (Proof shortened by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (𝐺 NeighbVtx 𝑁) ⊆ (𝑉 ∖ {𝑁})) | ||
Theorem | usgrnbssvwo2 26264 | The neighbors of a vertex in a simple graph are a subset of all vertices of the graph except the vertex itself and a vertex which is not a neighbor. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 27-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑀 ∉ (𝐺 NeighbVtx 𝑁)) → (𝐺 NeighbVtx 𝑁) ⊆ (𝑉 ∖ {𝑀, 𝑁})) | ||
Theorem | nbgrsym 26265 | A vertex in a graph is a neighbor of a second vertex iff the second vertex is a neighbor of the first vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 27-Oct-2020.) |
⊢ (𝐺 ∈ 𝑊 → (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ 𝐾 ∈ (𝐺 NeighbVtx 𝑁))) | ||
Theorem | nbupgrres 26266* | The neighborhood of a vertex in a restricted pseudograph (not necessarily valid for a hypergraph, because 𝑁, 𝐾 and 𝑀 could be connected by one edge, so 𝑀 is a neighbor of 𝐾 in the original graph, but not in the restricted graph, because the edge between 𝑀 and 𝐾, also incident with 𝑁, was removed). (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 8-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁}) ∧ 𝑀 ∈ (𝑉 ∖ {𝑁, 𝐾})) → (𝑀 ∈ (𝐺 NeighbVtx 𝐾) → 𝑀 ∈ (𝑆 NeighbVtx 𝐾))) | ||
Theorem | usgrnbcnvfv 26267 | Applying the edge function on the converse edge function applied on a pair of a vertex and one of its neighbors is this pair in a simple graph. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 27-Oct-2020.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ (𝐺 NeighbVtx 𝐾)) → (𝐼‘(◡𝐼‘{𝐾, 𝑁})) = {𝐾, 𝑁}) | ||
Theorem | nbusgredgeu 26268* | For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 27-Oct-2020.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑀 ∈ (𝐺 NeighbVtx 𝑁)) → ∃!𝑒 ∈ 𝐸 𝑒 = {𝑀, 𝑁}) | ||
Theorem | edgnbusgreu 26269* | For each edge incident to a vertex there is exactly one neighbor of the vertex also incident to this edge in a simple graph. (Contributed by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑀) ⇒ ⊢ (((𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑉) ∧ (𝐶 ∈ 𝐸 ∧ 𝑀 ∈ 𝐶)) → ∃!𝑛 ∈ 𝑁 𝐶 = {𝑀, 𝑛}) | ||
Theorem | nbusgredgeu0 26270* | For each neighbor of a vertex there is exactly one edge between the vertex and its neighbor in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 27-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑈) & ⊢ 𝐼 = {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} ⇒ ⊢ (((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) ∧ 𝑀 ∈ 𝑁) → ∃!𝑖 ∈ 𝐼 𝑖 = {𝑈, 𝑀}) | ||
Theorem | nbusgrf1o0 26271* | The mapping of neighbors of a vertex to edges incident to the vertex is a bijection ( 1-1 onto function) in a simple graph. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑈) & ⊢ 𝐼 = {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} & ⊢ 𝐹 = (𝑛 ∈ 𝑁 ↦ {𝑈, 𝑛}) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → 𝐹:𝑁–1-1-onto→𝐼) | ||
Theorem | nbusgrf1o1 26272* | The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑈) & ⊢ 𝐼 = {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ∃𝑓 𝑓:𝑁–1-1-onto→𝐼) | ||
Theorem | nbusgrf1o 26273* | The set of neighbors of a vertex is isomorphic to the set of edges containing the vertex in a simple graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ∃𝑓 𝑓:(𝐺 NeighbVtx 𝑈)–1-1-onto→{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒}) | ||
Theorem | nbedgusgr 26274* | The number of neighbors of a vertex is the number of edges at the vertex in a simple graph. (Contributed by AV, 27-Dec-2020.) (Proof shortened by AV, 5-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (#‘(𝐺 NeighbVtx 𝑈)) = (#‘{𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒})) | ||
Theorem | edgusgrnbfin 26275* | The number of neighbors of a vertex in a simple graph is finite iff the number of edges having this vertex as endpoint is finite. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((𝐺 NeighbVtx 𝑈) ∈ Fin ↔ {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} ∈ Fin)) | ||
Theorem | nbusgrfi 26276 | The class of neighbors of a vertex in a simple graph with a finite number of edges is a finite set. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝐸 ∈ Fin ∧ 𝑈 ∈ 𝑉) → (𝐺 NeighbVtx 𝑈) ∈ Fin) | ||
Theorem | nbfiusgrfi 26277 | The class of neighbors of a vertex in a finite simple graph is a finite set. (Contributed by Alexander van der Vekens, 7-Mar-2018.) (Revised by AV, 28-Oct-2020.) |
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ (Vtx‘𝐺)) → (𝐺 NeighbVtx 𝑁) ∈ Fin) | ||
Theorem | hashnbusgrnn0 26278 | The number of neighbors of a vertex in a finite simple graph is a nonnegative integer. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 15-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (#‘(𝐺 NeighbVtx 𝑈)) ∈ ℕ0) | ||
Theorem | nbfusgrlevtxm1 26279 | The number of neighbors of a vertex is at most the number of vertices of the graph minus 1 in a finite simple graph. (Contributed by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (#‘(𝐺 NeighbVtx 𝑈)) ≤ ((#‘𝑉) − 1)) | ||
Theorem | nbfusgrlevtxm2 26280 | If there is a vertex which is not a neighbor of another vertex, the number of neighbors of the other vertex is at most the number of vertices of the graph minus 2 in a finite simple graph. (Contributed by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈 ∧ 𝑀 ∉ (𝐺 NeighbVtx 𝑈))) → (#‘(𝐺 NeighbVtx 𝑈)) ≤ ((#‘𝑉) − 2)) | ||
Theorem | nbusgrvtxm1 26281 | If the number of neighbors of a vertex in a finite simple graph is the number of vertices of the graph minus 1, each vertex except the first mentioned vertex is a neighbor of this vertex. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((#‘(𝐺 NeighbVtx 𝑈)) = ((#‘𝑉) − 1) → ((𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈) → 𝑀 ∈ (𝐺 NeighbVtx 𝑈)))) | ||
Theorem | nb3grprlem1 26282 | Lemma 1 for nb3grpr 26284. (Contributed by Alexander van der Vekens, 15-Oct-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ USGraph ) & ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) & ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) ⇒ ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))) | ||
Theorem | nb3grprlem2 26283* | Lemma 2 for nb3grpr 26284. (Contributed by Alexander van der Vekens, 17-Oct-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ USGraph ) & ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) & ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤})) | ||
Theorem | nb3grpr 26284* | The neighbors of a vertex in a simple graph with three elements are an unordered pair of the other vertices iff all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ USGraph ) & ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) & ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ∀𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ (𝑉 ∖ {𝑦})(𝐺 NeighbVtx 𝑥) = {𝑦, 𝑧})) | ||
Theorem | nb3grpr2 26285 | The neighbors of a vertex in a simple graph with three elements are an unordered pair of the other vertices iff all vertices are connected with each other. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ USGraph ) & ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) & ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ∧ (𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵}))) | ||
Theorem | nb3gr2nb 26286 | If the neighbors of two vertices in a graph with three elements are an unordered pair of the other vertices, the neighbors of all three vertices are an unordered pair of the other vertices. (Contributed by Alexander van der Vekens, 18-Oct-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ ((Vtx‘𝐺) = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph )) → (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶}) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∧ (𝐺 NeighbVtx 𝐵) = {𝐴, 𝐶} ∧ (𝐺 NeighbVtx 𝐶) = {𝐴, 𝐵}))) | ||
Theorem | uvtxaval 26287* | The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 29-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)}) | ||
Theorem | uvtxael 26288* | A universal vertex, i.e. an element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 29-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑁})𝑛 ∈ (𝐺 NeighbVtx 𝑁)))) | ||
Theorem | uvtxaisvtx 26289 | A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → 𝑁 ∈ 𝑉) | ||
Theorem | uvtxassvtx 26290 | The set of the universal vertices is a subset of the set of all vertices. (Contributed by AV, 23-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (UnivVtx‘𝐺) ⊆ 𝑉 | ||
Theorem | vtxnbuvtx 26291* | A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → ∀𝑛 ∈ (𝑉 ∖ {𝑁})𝑛 ∈ (𝐺 NeighbVtx 𝑁)) | ||
Theorem | uvtxanbgr 26292 | A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → (𝑉 ∖ {𝑁}) ⊆ (𝐺 NeighbVtx 𝑁)) | ||
Theorem | uvtxanbgrvtx 26293* | A universal vertex is neighbor of all other vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → ∀𝑣 ∈ (𝑉 ∖ {𝑁})𝑁 ∈ (𝐺 NeighbVtx 𝑣)) | ||
Theorem | uvtxa0 26294 | There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑉 = ∅ → (UnivVtx‘𝐺) = ∅) | ||
Theorem | isuvtxa 26295* | The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑣})∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒}) | ||
Theorem | uvtxael1 26296* | A universal vertex, i.e. an element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁})∃𝑒 ∈ 𝐸 {𝑘, 𝑁} ⊆ 𝑒))) | ||
Theorem | uvtxa01vtx0 26297 | If a graph/class has no edges, it has universal vertices if and only if it has exactly one vertex. (Contributed by AV, 30-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → ((UnivVtx‘𝐺) ≠ ∅ ↔ (#‘𝑉) = 1)) | ||
Theorem | uvtxa01vtx 26298 | If a graph/class has no edges, it has universal vertices if and only if it has exactly one vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐸 = ∅ → ((UnivVtx‘𝐺) ≠ ∅ ↔ (#‘𝑉) = 1)) | ||
Theorem | uvtx2vtx1edg 26299* | If a graph has two vertices, and there is an edge between the vertices, then each vertex is universal. (Contributed by AV, 1-Nov-2020.) (Revised by AV, 25-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((#‘𝑉) = 2 ∧ 𝑉 ∈ 𝐸) → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺)) | ||
Theorem | uvtx2vtx1edgb 26300* | If a hypergraph has two vertices, there is an edge between the vertices iff each vertex is universal. (Contributed by AV, 3-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (#‘𝑉) = 2) → (𝑉 ∈ 𝐸 ↔ ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |