![]() |
Metamath
Proof Explorer Theorem List (p. 291 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | uhgrissubgr 29001 | The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝑆) & ⊢ 𝐴 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝑆) & ⊢ 𝐵 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵))) | ||
Theorem | subgrprop3 29002 | The properties of a subgraph: If 𝑆 is a subgraph of 𝐺, its vertices are also vertices of 𝐺, and its edges are also edges of 𝐺. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝑆) & ⊢ 𝐴 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝑆) & ⊢ 𝐵 = (Edg‘𝐺) ⇒ ⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵)) | ||
Theorem | egrsubgr 29003 | An empty graph consisting of a subset of vertices of a graph (and having no edges) is a subgraph of the graph. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 17-Dec-2020.) |
⊢ (((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈) ∧ (Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (Fun (iEdg‘𝑆) ∧ (Edg‘𝑆) = ∅)) → 𝑆 SubGraph 𝐺) | ||
Theorem | 0grsubgr 29004 | The null graph (represented by an empty set) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.) |
⊢ (𝐺 ∈ 𝑊 → ∅ SubGraph 𝐺) | ||
Theorem | 0uhgrsubgr 29005 | The null graph (as hypergraph) is a subgraph of all graphs. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 28-Nov-2020.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ∧ (Vtx‘𝑆) = ∅) → 𝑆 SubGraph 𝐺) | ||
Theorem | uhgrsubgrself 29006 | A hypergraph is a subgraph of itself. (Contributed by AV, 17-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
⊢ (𝐺 ∈ UHGraph → 𝐺 SubGraph 𝐺) | ||
Theorem | subgrfun 29007 | The edge function of a subgraph of a graph whose edge function is actually a function is a function. (Contributed by AV, 20-Nov-2020.) |
⊢ ((Fun (iEdg‘𝐺) ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) | ||
Theorem | subgruhgrfun 29008 | The edge function of a subgraph of a hypergraph is a function. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 20-Nov-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) | ||
Theorem | subgreldmiedg 29009 | An element of the domain of the edge function of a subgraph is an element of the domain of the edge function of the supergraph. (Contributed by AV, 20-Nov-2020.) |
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom (iEdg‘𝑆)) → 𝑋 ∈ dom (iEdg‘𝐺)) | ||
Theorem | subgruhgredgd 29010 | An edge of a subgraph of a hypergraph is a nonempty subset of its vertices. (Contributed by AV, 17-Nov-2020.) (Revised by AV, 21-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝑆) & ⊢ 𝐼 = (iEdg‘𝑆) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝑆 SubGraph 𝐺) & ⊢ (𝜑 → 𝑋 ∈ dom 𝐼) ⇒ ⊢ (𝜑 → (𝐼‘𝑋) ∈ (𝒫 𝑉 ∖ {∅})) | ||
Theorem | subumgredg2 29011* | An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝑆) & ⊢ 𝐼 = (iEdg‘𝑆) ⇒ ⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) | ||
Theorem | subuhgr 29012 | A subgraph of a hypergraph is a hypergraph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UHGraph) | ||
Theorem | subupgr 29013 | A subgraph of a pseudograph is a pseudograph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UPGraph) | ||
Theorem | subumgr 29014 | A subgraph of a multigraph is a multigraph. (Contributed by AV, 26-Nov-2020.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UMGraph) | ||
Theorem | subusgr 29015 | A subgraph of a simple graph is a simple graph. (Contributed by AV, 16-Nov-2020.) (Proof shortened by AV, 27-Nov-2020.) |
⊢ ((𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ USGraph) | ||
Theorem | uhgrspansubgrlem 29016 | Lemma for uhgrspansubgr 29017: The edges of the graph 𝑆 obtained by removing some edges of a hypergraph 𝐺 are subsets of its vertices (a spanning subgraph, see comment for uhgrspansubgr 29017. (Contributed by AV, 18-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) ⇒ ⊢ (𝜑 → (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆)) | ||
Theorem | uhgrspansubgr 29017 | A spanning subgraph 𝑆 of a hypergraph 𝐺 is actually a subgraph of 𝐺. A subgraph 𝑆 of a graph 𝐺 which has the same vertices as 𝐺 and is obtained by removing some edges of 𝐺 is called a spanning subgraph (see section I.1 in [Bollobas] p. 2 and section 1.1 in [Diestel] p. 4). Formally, the edges are "removed" by restricting the edge function of the original graph by an arbitrary class (which actually needs not to be a subset of the domain of the edge function). (Contributed by AV, 18-Nov-2020.) (Proof shortened by AV, 21-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ UHGraph) ⇒ ⊢ (𝜑 → 𝑆 SubGraph 𝐺) | ||
Theorem | uhgrspan 29018 | 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 29019 | 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 29020 | A spanning subgraph 𝑆 of a multigraph 𝐺 is a multigraph. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐸 ↾ 𝐴)) & ⊢ (𝜑 → 𝐺 ∈ UMGraph) ⇒ ⊢ (𝜑 → 𝑆 ∈ UMGraph) | ||
Theorem | usgrspan 29021 | 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 29022 | 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 29023 | 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 29024 | 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 29025 | 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 29026 | Lemma 1 for uhgrspan1 29029. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)} ⇒ ⊢ ((𝑉 ∖ {𝑁}) ∈ V ∧ (𝐼 ↾ 𝐹) ∈ V) | ||
Theorem | uhgrspan1lem2 29027 | Lemma 2 for uhgrspan1 29029. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)〉 ⇒ ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁}) | ||
Theorem | uhgrspan1lem3 29028 | Lemma 3 for uhgrspan1 29029. (Contributed by AV, 19-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ (𝐼‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐼 ↾ 𝐹)〉 ⇒ ⊢ (iEdg‘𝑆) = (𝐼 ↾ 𝐹) | ||
Theorem | uhgrspan1 29029* | 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 29030* | Lemma for upgrres 29032. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣ (♯‘𝑝) ≤ 2}) | ||
Theorem | umgrreslem 29031* | Lemma for umgrres 29033 and usgrres 29034. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (♯‘𝑝) = 2}) | ||
Theorem | upgrres 29032* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a pseudograph (see uhgrspan1 29029) is a pseudograph. (Contributed by AV, 8-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph) | ||
Theorem | umgrres 29033* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a multigraph (see uhgrspan1 29029) is a multigraph. (Contributed by AV, 27-Nov-2020.) (Revised by AV, 19-Dec-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), (𝐸 ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph) | ||
Theorem | usgrres 29034* | A subgraph obtained by removing one vertex and all edges incident with this vertex from a simple graph (see uhgrspan1 29029) 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 29035* | Lemma 1 for upgrres1 29039. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝑉 ∖ {𝑁}) ∈ V ∧ ( I ↾ 𝐹) ∈ V) | ||
Theorem | umgrres1lem 29036* | Lemma for umgrres1 29040. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ran ( I ↾ 𝐹) ⊆ {𝑝 ∈ 𝒫 (𝑉 ∖ {𝑁}) ∣ (♯‘𝑝) = 2}) | ||
Theorem | upgrres1lem2 29037* | Lemma 2 for upgrres1 29039. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (Vtx‘𝑆) = (𝑉 ∖ {𝑁}) | ||
Theorem | upgrres1lem3 29038* | Lemma 3 for upgrres1 29039. (Contributed by AV, 7-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ (iEdg‘𝑆) = ( I ↾ 𝐹) | ||
Theorem | upgrres1 29039* | 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 28994 since the domains of the edge functions may not be compatible. (Contributed by AV, 8-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UPGraph) | ||
Theorem | umgrres1 29040* | 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 28994 since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐹 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒} & ⊢ 𝑆 = 〈(𝑉 ∖ {𝑁}), ( I ↾ 𝐹)〉 ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → 𝑆 ∈ UMGraph) | ||
Theorem | usgrres1 29041* | 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 28994 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 29042 | Extend class notation with finite simple graphs. |
class FinUSGraph | ||
Definition | df-fusgr 29043 | 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 29044 | 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 29045 | A finite simple graph has a finite set of vertices. (Contributed by AV, 16-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin) | ||
Theorem | isfusgrf1 29046* | 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 29047 | 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 29048 | A finite simple graph is a simple graph. (Contributed by AV, 16-Jan-2020.) (Revised by AV, 21-Oct-2020.) |
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph) | ||
Theorem | opfusgr 29049 | A finite simple graph represented as ordered pair. (Contributed by AV, 23-Oct-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (〈𝑉, 𝐸〉 ∈ FinUSGraph ↔ (〈𝑉, 𝐸〉 ∈ USGraph ∧ 𝑉 ∈ Fin))) | ||
Theorem | usgredgffibi 29050 | 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 29051* | 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 29052 | 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 29053* | 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 29054 | Induction base for fusgrfis 29056. Main work is done in uhgr0v0e 28964. (Contributed by Alexander van der Vekens, 5-Jan-2018.) (Revised by AV, 23-Oct-2020.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ 〈𝑉, 𝐸〉 ∈ USGraph ∧ (♯‘𝑉) = 0) → 𝐸 ∈ Fin) | ||
Theorem | fusgrfisstep 29055* | Induction step in fusgrfis 29056: 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 29056 | 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 29057 | 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 29058 | Extend class notation with neighbors (of a vertex in a graph). |
class NeighbVtx | ||
Definition | df-nbgr 29059* |
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 22924), 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 29060 | 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 29061 | 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 29062* | 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 29063* | 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 29064* | Alternate definition of the neighbors of a vertex using the edge function instead of the edges themselves (see also nbgrval 29062). (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 29065 | 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 29066* | 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 29067 | 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 29068 | 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 29069* | The set of neighbors of a vertex in a hypergraph. This version of nbgrval 29062 (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 29070* | 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 29071 | A neighbor of a vertex in a pseudograph. (Contributed by AV, 5-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉) ∧ (𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 𝐾)) → (𝑁 ∈ (𝐺 NeighbVtx 𝐾) ↔ {𝑁, 𝐾} ∈ 𝐸)) | ||
Theorem | nbumgrvtx 29072* | 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 29073* | The set of neighbors of an arbitrary class in a multigraph. (Contributed by AV, 27-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → (𝐺 NeighbVtx 𝑁) = {𝑛 ∈ 𝑉 ∣ {𝑁, 𝑛} ∈ 𝐸}) | ||
Theorem | nbusgrvtx 29074* | 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 29075* | 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 29076* | 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 29077* | Lemma for nbuhgr2vtx1edgb 29078. This reverse direction of nbgr2vtx1edg 29076 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 29078* | 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 29079 | 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 29080* | 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 29081* | Lemma for nbgr0vtx 29082 and nbgr0edg 29083. (Contributed by AV, 15-Nov-2020.) |
⊢ (𝜑 → ∀𝑛 ∈ ((Vtx‘𝐺) ∖ {𝐾}) ¬ ∃𝑒 ∈ (Edg‘𝐺){𝐾, 𝑛} ⊆ 𝑒) ⇒ ⊢ (𝜑 → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr0vtx 29082 | In a null graph (with no vertices), all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
⊢ ((Vtx‘𝐺) = ∅ → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgr0edg 29083 | 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 29084 | In a graph with one vertex, all neighborhoods are empty. (Contributed by AV, 15-Nov-2020.) |
⊢ ((♯‘(Vtx‘𝐺)) = 1 → (𝐺 NeighbVtx 𝐾) = ∅) | ||
Theorem | nbgrnself 29085* | 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 29086 | 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 29087 | The neighbors of a vertex 𝑋 form a subset of all vertices except the vertex 𝑋 itself. Stronger version of nbgrssvtx 29068. (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 29088 | 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 29089 | 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 29090* | 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 29091 | 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 29092* | 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 29093* | 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 29094* | 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 29095* | 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 29096* | 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 29097* | 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 29098* | 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 29099* | 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 29100 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |