Home | Metamath
Proof Explorer Theorem List (p. 271 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uhgrspan 27001 | A spanning subgraph 𝑆 of a hypergraph 𝐺 is a hypergraph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) ⇒ ⊢ (𝜑 → 𝑆 ∈ UHGraph) | ||
Theorem | upgrspan 27002 | A spanning subgraph 𝑆 of a pseudograph 𝐺 is a pseudograph. (Contributed by AV, 11-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) ⇒ ⊢ (𝜑 → 𝑆 ∈ UPGraph) | ||
Theorem | umgrspan 27003 | A spanning subgraph 𝑆 of a multigraph 𝐺 is a multigraph. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ UMGraph) ⇒ ⊢ (𝜑 → 𝑆 ∈ UMGraph) | ||
Theorem | usgrspan 27004 | A spanning subgraph 𝑆 of a simple graph 𝐺 is a simple graph. (Contributed by AV, 15-Oct-2020.) (Revised by AV, 16-Oct-2020.) (Proof shortened by AV, 18-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ USGraph) ⇒ ⊢ (𝜑 → 𝑆 ∈ USGraph) | ||
Theorem | uhgrspanop 27005 | A spanning subgraph of a hypergraph represented by an ordered pair is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → 〈𝑉, (𝐸 ↾ 𝐴)〉 ∈ UHGraph) | ||
Theorem | upgrspanop 27006 | A spanning subgraph of a pseudograph represented by an ordered pair is a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 13-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → 〈𝑉, (𝐸 ↾ 𝐴)〉 ∈ UPGraph) | ||
Theorem | umgrspanop 27007 | A spanning subgraph of a multigraph represented by an ordered pair is a multigraph. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → 〈𝑉, (𝐸 ↾ 𝐴)〉 ∈ UMGraph) | ||
Theorem | usgrspanop 27008 | A spanning subgraph of a simple graph represented by an ordered pair is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Revised by AV, 16-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → 〈𝑉, (𝐸 ↾ 𝐴)〉 ∈ USGraph) | ||
Theorem | uhgrspan1lem1 27009 | Lemma 1 for uhgrspan1 27012. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)} ⇒ ⊢ ((𝑉 ∖ {𝑁}) ∈ V ∧ (𝐼 ↾ 𝐹) ∈ V) | ||
Theorem | uhgrspan1lem2 27010 | Lemma 2 for uhgrspan1 27012. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)〉 ⇒ ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁}) | ||
Theorem | uhgrspan1lem3 27011 | Lemma 3 for uhgrspan1 27012. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)〉 ⇒ ⊢ (iEdg‘𝑆) = (𝐼 ↾ 𝐹) | ||
Theorem | uhgrspan1 27012* | The induced subgraph 𝑆 of a hypergraph 𝐺 obtained by removing one vertex is actually a subgraph of 𝐺. A subgraph is called induced or spanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 SubGraph 𝐺) | ||
Theorem | upgrreslem 27013* | Lemma for upgrres 27015. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣ (♯‘𝑝) ≤ 2}) | ||
Theorem | umgrreslem 27014* | Lemma for umgrres 27016 and usgrres 27017. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (♯‘𝑝) = 2}) | ||
Theorem | upgrres 27015* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 27012) is a pseudograph. (Contributed by AV, 8-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph) | ||
Theorem | umgrres 27016* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 27012) is a multigraph. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph) | ||
Theorem | usgrres 27017* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a simple graph (see uhgrspan1 27012) is a simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ USGraph) | ||
Theorem | upgrres1lem1 27018* | Lemma 1 for upgrres1 27022. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝑉 ∖ {𝑁}) ∈ V ∧ ( I ↾ 𝐹) ∈ V) | ||
Theorem | umgrres1lem 27019* | Lemma for umgrres1 27023. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ran ( I ↾ 𝐹) ⊆ {𝑝 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (♯‘𝑝) = 2}) | ||
Theorem | upgrres1lem2 27020* | Lemma 2 for upgrres1 27022. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁}) | ||
Theorem | upgrres1lem3 27021* | Lemma 3 for upgrres1 27022. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (iEdg‘𝑆) = ( I ↾ 𝐹) | ||
Theorem | upgrres1 27022* | 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 26977 since the domains of the edge functions may not be compatible. (Contributed by AV, 8-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph) | ||
Theorem | umgrres1 27023* | 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 26977 since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph) | ||
Theorem | usgrres1 27024* | 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 26977 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 27025 | Extend class notation with finite simple graphs. |
class FinUSGraph | ||
Definition | df-fusgr 27026 | 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 27027 | 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 27028 | A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) | ||
Theorem | isfusgrf1 27029* | 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 27030 | 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 27031 | A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph) | ||
Theorem | opfusgr 27032 | A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (〈𝑉, 𝐸〉 ∈ FinUSGraph ↔ (〈𝑉, 𝐸〉 ∈ USGraph ∧ 𝑉 ∈ Fin))) | ||
Theorem | usgredgffibi 27033 | 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 27034* | 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 27035 | 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 27036* | 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 27037 | Induction base for fusgrfis 27039. Main work is done in uhgr0v0e 26947. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 〈𝑉, 𝐸〉 ∈ USGraph ∧ (♯‘𝑉) = 0) → 𝐸 ∈ Fin) | ||
Theorem | fusgrfisstep 27038* | Induction step in fusgrfis 27039: 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 27039 | 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 27040 | 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 27041 | Extend class notation with neighbors (of a vertex in a graph). |
class NeighbVtx | ||
Definition | df-nbgr 27042* |
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 21634), 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 27043 | 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 27044 | 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 27045* | 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 27046* | 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 27047* | Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval 27045). (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 27048 | 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 27049* | 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 27050 | 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 27051 | 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 27052* | The set of neighbors of a vertex in a hypergraph. This version of nbgrval 27045 (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 27053* | 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 27054 | A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾)) → (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑁, 𝐾} ∈ 𝐸)) | ||
Theorem | nbumgrvtx 27055* | 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 27056* | The set of neighbors of an arbitrary class in a multigraph. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) | ||
Theorem | nbusgrvtx 27057* | 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 27058* | 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 27059* | 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 27060* | Lemma for nbuhgr2vtx1edgb 27061. This reverse direction of nbgr2vtx1edg 27059 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 27061* | 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 27062 | 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 27063* | 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 27064* | Lemma for nbgr0vtx 27065 and nbgr0edg 27066. (Contributed by AV, 15-Nov-2020.) |
⊢ (𝜑 → ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝐾}) ¬ ∃𝑒 ∈ (Edg‘𝐺){𝐾, 𝑛} ⊆ 𝑒) ⇒ ⊢ (𝜑 → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr0vtx 27065 | In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr0edg 27066 | 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 27067 | In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
⊢ ((♯‘(Vtx‘𝐺)) = 1 → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgrnself 27068* | 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 27069 | 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 27070 | The neighbors of a vertex 𝑋 form a subset of all vertices except the vertex 𝑋 itself. Stronger version of nbgrssvtx 27051. (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 27071 | 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 27072 | 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 27073* | 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 27074 | 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 27075* | 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 27076* | 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 27077* | 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 27078* | 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 27079* | 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 27080* | 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 27081* | 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 27082* | 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 27083 | 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 27084 | 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 27085 | 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 27086 | 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 27087 | 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 27088 | 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 27089 | Lemma 1 for nb3grpr 27091. (Contributed by Alexander van der Vekens, 15-Oct-2017.) (Revised by AV, 28-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ USGraph) & ⊢ (𝜑 → 𝑉 = {𝐴, 𝐵, 𝐶}) & ⊢ (𝜑 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) ⇒ ⊢ (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐴, 𝐶} ∈ 𝐸))) | ||
Theorem | nb3grprlem2 27090* | Lemma 2 for nb3grpr 27091. (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 27091* | 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 27092 | 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 27093 | 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 27094 | Extend class notation with the universal vertices (in a graph). |
class UnivVtx | ||
Definition | df-uvtx 27095* | 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 27096* | 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 27097* | 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 27098 | 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 27099 | 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 27100* | 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 𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |