![]() |
Metamath
Proof Explorer Theorem List (p. 272 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | upgrres1lem2 27101* | Lemma 2 for upgrres1 27103. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁}) | ||
Theorem | upgrres1lem3 27102* | Lemma 3 for upgrres1 27103. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (iEdg‘𝑆) = ( I ↾ 𝐹) | ||
Theorem | upgrres1 27103* | 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 27058 since the domains of the edge functions may not be compatible. (Contributed by AV, 8-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph) | ||
Theorem | umgrres1 27104* | 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 27058 since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph) | ||
Theorem | usgrres1 27105* | 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 27058 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 27106 | Extend class notation with finite simple graphs. |
class FinUSGraph | ||
Definition | df-fusgr 27107 | 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 27108 | 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 27109 | A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) | ||
Theorem | isfusgrf1 27110* | 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 27111 | 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 27112 | A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph) | ||
Theorem | opfusgr 27113 | A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (〈𝑉, 𝐸〉 ∈ FinUSGraph ↔ (〈𝑉, 𝐸〉 ∈ USGraph ∧ 𝑉 ∈ Fin))) | ||
Theorem | usgredgffibi 27114 | 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 27115* | 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 27116 | 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 27117* | 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 27118 | Induction base for fusgrfis 27120. Main work is done in uhgr0v0e 27028. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 〈𝑉, 𝐸〉 ∈ USGraph ∧ (♯‘𝑉) = 0) → 𝐸 ∈ Fin) | ||
Theorem | fusgrfisstep 27119* | Induction step in fusgrfis 27120: 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 27120 | 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 27121 | 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 27122 | Extend class notation with neighbors (of a vertex in a graph). |
class NeighbVtx | ||
Definition | df-nbgr 27123* |
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 21703), 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 27124 | The set of neighbors is empty if the graph 𝐺 or the vertex 𝑁 are proper classes. (Contributed by AV, 26-Oct-2020.) |
⊢ (¬ (𝐺 ∈ V ∧ 𝑁 ∈ V) → (𝐺 NeighbVtx 𝑁) = ∅) | ||
Theorem | nbgrcl 27125 | If a class 𝑋 has at least one neighbor, this class must be a vertex. (Contributed by AV, 6-Jun-2021.) (Revised by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝑋) → 𝑋 ∈ 𝑉) | ||
Theorem | nbgrval 27126* | 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 27127* | 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 27128* | Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval 27126). (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 27129 | If a class 𝑋 is not a vertex of a graph 𝐺, then it has no neighbors in 𝐺. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑋 ∉ 𝑉 → (𝐺 NeighbVtx 𝑋) = ∅) | ||
Theorem | nbgrel 27130* | 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.) (Revised by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝑋) ↔ ((𝑁 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ 𝑁 ≠ 𝑋 ∧ ∃𝑒 ∈ 𝐸 {𝑋, 𝑁} ⊆ 𝑒)) | ||
Theorem | nbgrisvtx 27131 | Every neighbor 𝑁 of a vertex 𝐾 is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Revised by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝐾) → 𝑁 ∈ 𝑉) | ||
Theorem | nbgrssvtx 27132 | The neighbors of a vertex 𝐾 in a graph form a subset of all vertices of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 26-Oct-2020.) (Revised by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 NeighbVtx 𝐾) ⊆ 𝑉 | ||
Theorem | nbuhgr 27133* | The set of neighbors of a vertex in a hypergraph. This version of nbgrval 27126 (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 27134* | 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 27135 | A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾)) → (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑁, 𝐾} ∈ 𝐸)) | ||
Theorem | nbumgrvtx 27136* | 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 27137* | The set of neighbors of an arbitrary class in a multigraph. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) | ||
Theorem | nbusgrvtx 27138* | 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 27139* | 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 27140* | 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.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((♯‘𝑉) = 2 ∧ 𝑉 ∈ 𝐸) → ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)) | ||
Theorem | nbuhgr2vtx1edgblem 27141* | Lemma for nbuhgr2vtx1edgb 27142. This reverse direction of nbgr2vtx1edg 27140 only holds for classes whose edges are subsets of the set of vertices, which is the property of hypergraphs. (Contributed by AV, 2-Nov-2020.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑉 = {𝑎, 𝑏} ∧ 𝑎 ∈ (𝐺 NeighbVtx 𝑏)) → {𝑎, 𝑏} ∈ 𝐸) | ||
Theorem | nbuhgr2vtx1edgb 27142* | 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.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ (♯‘𝑉) = 2) → (𝑉 ∈ 𝐸 ↔ ∀𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))) | ||
Theorem | nbusgreledg 27143 | 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 27144* | 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 27145* | Lemma for nbgr0vtx 27146 and nbgr0edg 27147. (Contributed by AV, 15-Nov-2020.) |
⊢ (𝜑 → ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝐾}) ¬ ∃𝑒 ∈ (Edg‘𝐺){𝐾, 𝑛} ⊆ 𝑒) ⇒ ⊢ (𝜑 → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr0vtx 27146 | In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr0edg 27147 | 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 27148 | In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
⊢ ((♯‘(Vtx‘𝐺)) = 1 → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgrnself 27149* | A vertex in a graph is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ∀𝑣 ∈ 𝑉 𝑣 ∉ (𝐺 NeighbVtx 𝑣) | ||
Theorem | nbgrnself2 27150 | 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.) (Revised by AV, 12-Feb-2022.) |
⊢ 𝑋 ∉ (𝐺 NeighbVtx 𝑋) | ||
Theorem | nbgrssovtx 27151 | The neighbors of a vertex 𝑋 form a subset of all vertices except the vertex 𝑋 itself. Stronger version of nbgrssvtx 27132. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 NeighbVtx 𝑋) ⊆ (𝑉 ∖ {𝑋}) | ||
Theorem | nbgrssvwo2 27152 | The neighbors of a vertex 𝑋 form a subset of all vertices except the vertex 𝑋 itself and a class 𝑀 which is not a neighbor of 𝑋. (Contributed by Alexander van der Vekens, 13-Jul-2018.) (Revised by AV, 3-Nov-2020.) (Revised by AV, 12-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑀 ∉ (𝐺 NeighbVtx 𝑋) → (𝐺 NeighbVtx 𝑋) ⊆ (𝑉 ∖ {𝑀, 𝑋})) | ||
Theorem | nbgrsym 27153 | In a graph, the neighborhood relation is symmetric: 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.) (Revised by AV, 12-Feb-2022.) |
⊢ (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ 𝐾 ∈ (𝐺 NeighbVtx 𝑁)) | ||
Theorem | nbupgrres 27154* | 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 27155 | 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 27156* | 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 27157* | 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.) (Revised by AV, 6-Jul-2022.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑀) ⇒ ⊢ (((𝐺 ∈ USGraph ∧ 𝑀 ∈ 𝑉) ∧ (𝐶 ∈ 𝐸 ∧ 𝑀 ∈ 𝐶)) → ∃!𝑛 ∈ 𝑁 𝐶 = {𝑀, 𝑛}) | ||
Theorem | nbusgredgeu0 27158* | 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.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑁 = (𝐺 NeighbVtx 𝑈) & ⊢ 𝐼 = {𝑒 ∈ 𝐸 ∣ 𝑈 ∈ 𝑒} ⇒ ⊢ (((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) ∧ 𝑀 ∈ 𝑁) → ∃!𝑖 ∈ 𝐼 𝑖 = {𝑈, 𝑀}) | ||
Theorem | nbusgrf1o0 27159* | 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 27160* | 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 27161* | 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 27162* | 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 27163* | 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 27164 | 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 27165 | 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 27166 | 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 27167 | 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.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 1)) | ||
Theorem | nbfusgrlevtxm2 27168 | 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.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) ∧ (𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑈 ∧ 𝑀 ∉ (𝐺 NeighbVtx 𝑈))) → (♯‘(𝐺 NeighbVtx 𝑈)) ≤ ((♯‘𝑉) − 2)) | ||
Theorem | nbusgrvtxm1 27169 | 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 27170 | Lemma 1 for nb3grpr 27172. (Contributed by Alexander van der Vekens, 15-Oct-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ USGraph) & ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) & ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) ⇒ ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))) | ||
Theorem | nb3grprlem2 27171* | Lemma 2 for nb3grpr 27172. (Contributed by Alexander van der Vekens, 17-Oct-2017.) (Revised by AV, 28-Oct-2020.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ USGraph) & ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) & ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) & ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ⇒ ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣 ∈ 𝑉 ∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤})) | ||
Theorem | nb3grpr 27172* | 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 27173 | 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 27174 | 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 𝐶) = {𝐴, 𝐵}))) | ||
Syntax | cuvtx 27175 | Extend class notation with the universal vertices (in a graph). |
class UnivVtx | ||
Definition | df-uvtx 27176* | 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), or equivalently, if 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 𝑣)}) | ||
Theorem | uvtxval 27177* | The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 29-Oct-2020.) (Revised by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} | ||
Theorem | uvtxel 27178* | 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.) (Revised by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑁})𝑛 ∈ (𝐺 NeighbVtx 𝑁))) | ||
Theorem | uvtxisvtx 27179 | A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) (Proof shortened by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → 𝑁 ∈ 𝑉) | ||
Theorem | uvtxssvtx 27180 | 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 27181* | A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.) (Revised by AV, 30-Oct-2020.) (Proof shortened by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) → ∀𝑛 ∈ (𝑉 ∖ {𝑁})𝑛 ∈ (𝐺 NeighbVtx 𝑁)) | ||
Theorem | uvtxnbgrss 27182 | 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 | uvtxnbgrvtx 27183* | 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 | uvtx0 27184 | 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.) (Proof shortened by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑉 = ∅ → (UnivVtx‘𝐺) = ∅) | ||
Theorem | isuvtx 27185* | The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 30-Oct-2020.) (Revised by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑘 ∈ (𝑉 ∖ {𝑣})∃𝑒 ∈ 𝐸 {𝑘, 𝑣} ⊆ 𝑒} | ||
Theorem | uvtxel1 27186* | Characterization of a universal vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.) (Revised by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝑁 ∈ 𝑉 ∧ ∀𝑘 ∈ (𝑉 ∖ {𝑁})∃𝑒 ∈ 𝐸 {𝑘, 𝑁} ⊆ 𝑒)) | ||
Theorem | uvtx01vtx 27187 | 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.) (Revised by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐸 = ∅ → ((UnivVtx‘𝐺) ≠ ∅ ↔ (♯‘𝑉) = 1)) | ||
Theorem | uvtx2vtx1edg 27188* | 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.) (Proof shortened by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((♯‘𝑉) = 2 ∧ 𝑉 ∈ 𝐸) → ∀𝑣 ∈ 𝑉 𝑣 ∈ (UnivVtx‘𝐺)) | ||
Theorem | uvtx2vtx1edgb 27189* | 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‘𝐺))) | ||
Theorem | uvtxnbgr 27190 | 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 27191 | 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.) (Proof shortened by AV, 14-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝑁 ∈ (UnivVtx‘𝐺) ↔ (𝐺 NeighbVtx 𝑁) = (𝑉 ∖ {𝑁}))) | ||
Theorem | uvtxusgr 27192* | 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 27193* | 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 | uvtxnm1nbgr 27194 | 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 27195 | 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.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → ((♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1) → 𝑈 ∈ (UnivVtx‘𝐺))) | ||
Theorem | uvtxnbvtxm1 27196 | A universal vertex has 𝑛 − 1 neighbors in a finite simple graph with 𝑛 vertices. A biconditional version of nbusgrvtxm1uvtx 27195 resp. uvtxnm1nbgr 27194. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (𝑈 ∈ (UnivVtx‘𝐺) ↔ (♯‘(𝐺 NeighbVtx 𝑈)) = ((♯‘𝑉) − 1))) | ||
Theorem | nbupgruvtxres 27197* | 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.) (Proof shortened by AV, 13-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝐾 ∈ (𝑉 ∖ {𝑁})) → ((𝐺 NeighbVtx 𝐾) = (𝑉 ∖ {𝐾}) → (𝑆 NeighbVtx 𝐾) = (𝑉 ∖ {𝑁, 𝐾}))) | ||
Theorem | uvtxupgrres 27198* | 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‘𝑆))) | ||
Syntax | ccplgr 27199 | Extend class notation with (arbitrary) complete graphs. |
class ComplGraph | ||
Syntax | ccusgr 27200 | Extend class notation with complete simple graphs. |
class ComplUSGraph |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |