SimpleGraph.ComponentCompl.subset_hom
theorem SimpleGraph.ComponentCompl.subset_hom :
∀ {V : Type u} {G : SimpleGraph V} {K L : Set V} (C : G.ComponentCompl L) (h : K ⊆ L),
↑C ⊆ ↑(SimpleGraph.ComponentCompl.hom h C)
The theorem `SimpleGraph.ComponentCompl.subset_hom` states that for any type `V`, simple graph `G` of type `V`, and sets `K` and `L` of type `V`, given a component `C` that lies outside of set `L` in graph `G` and a proof `h` that set `K` is a subset of `L`, the component `C` is a subset of the component outside of `K` that contains all components outside of `L`. This theorem essentially demonstrates the relationship between two components that lie outside different sets in a simple graph, given a certain subset relationship between these sets.
More concisely: Given a simple graph and sets K and L with C a component of the graph outside L, if K is a subset of L, then C is a subset of the component outside K containing all components outside L.
|
SimpleGraph.ComponentCompl.ind
theorem SimpleGraph.ComponentCompl.ind :
∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {β : G.ComponentCompl K → Prop},
(∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)) → ∀ (C : G.ComponentCompl K), β C
The theorem `SimpleGraph.ComponentCompl.ind` is a principle of induction for components outside a given set of vertices in a simple graph. Given a type `V`, a simple graph `G` on `V`, a set `K` of `V`, and a property `β` that applies to components outside of `K`, if `β` holds for all vertices `v` that do not belong to `K` when they are considered as such components (constructed with `SimpleGraph.componentComplMk`), then `β` holds for any component outside of `K` in the graph. In other words, if the property holds for every individual vertex not in `K` when we consider it as a component outside `K`, then the property holds for any connected component outside of `K`.
More concisely: If a property holds for all vertices not in a set `K` when considered as components outside `K` in a simple graph `G`, then the property holds for any component outside of `K` in `G`.
|
SimpleGraph.ComponentCompl.mem_of_adj
theorem SimpleGraph.ComponentCompl.mem_of_adj :
∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {C : G.ComponentCompl K} (c d : V),
c ∈ C → d ∉ K → G.Adj c d → d ∈ C
This theorem states that for any type `V`, any simple graph `G` defined on `V`, any set `K` of vertices of `V`, and any component `C` of the graph `G` that is not in `K`, if a vertex `c` belongs to `C` and another vertex `d` does not belong to `K` and is adjacent to `c` (there is an edge between `c` and `d` in the graph `G`), then `d` must belong to `C`. In other words, any vertex that is adjacent to a vertex in a component of the graph not included in a certain set, and which itself is not in that set, must be part of the same component.
More concisely: If a simple graph G has a component C not in a set K of vertices, then for any vertex c in C and any adjacent vertex d not in K, we have d ∈ C.
|
SimpleGraph.ComponentCompl.disjoint_right
theorem SimpleGraph.ComponentCompl.disjoint_right :
∀ {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K), Disjoint K ↑C
This theorem states that for any type `V`, any `SimpleGraph` `G` on `V`, and any set `K` of vertices from `V`, if `C` is a component of the graph `G` induced by the complement of `K`, then `K` and `C` are disjoint. This can be interpreted as `K` and the component `C` having no common elements. In the context of a lattice, two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element. Here, `K` and `C` are disjoint in the sense that there is no vertex that belongs to both `K` and `C`.
More concisely: For any simple graph `G` on type `V`, and any set `K` of vertices from `V`, if `C` is a component of `G` induced by the complement of `K`, then `K` and `C` have no common elements.
|
SimpleGraph.ComponentCompl.nonempty
theorem SimpleGraph.ComponentCompl.nonempty :
∀ {V : Type u} {G : SimpleGraph V} {K : Set V} (C : G.ComponentCompl K), (↑C).Nonempty
This theorem states that for any type `V`, any simple graph `G` of type `V`, and any set `K` of vertices in `V`, if `C` is the set of vertices that are in the connected component of the graph induced by the complement of `K` in `G` (denoted as `SimpleGraph.ComponentCompl G K`), then `C` is not an empty set (expressed as `Set.Nonempty ↑C`). In other words, there exists at least one vertex in the connected component of the graph outside the set `K`.
More concisely: For any simple graph `G` of type `V` and any set `K` of vertices in `V` of `G`, the connected component of the complement of `K` in `G` is non-empty.
|
SimpleGraph.ComponentCompl.exists_adj_boundary_pair
theorem SimpleGraph.ComponentCompl.exists_adj_boundary_pair :
∀ {V : Type u} {G : SimpleGraph V} {K : Set V},
G.Preconnected → K.Nonempty → ∀ (C : G.ComponentCompl K), ∃ ck, ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
The theorem `SimpleGraph.ComponentCompl.exists_adj_boundary_pair` states that for any given type `V`, graph `G` of this type, and set `K` of this type, provided that graph `G` is preconnected and set `K` is not empty, for any connected component `C` that is not in `K`, there exists a pair of vertices `(ck.1, ck.2)` such that `ck.1` is in `C`, `ck.2` is in `K`, and `ck.1` and `ck.2` are adjacent in the graph `G`.
More concisely: For any preconnected graph `G` on type `V` and non-empty set `K` of vertices, every connected component `C` not in `K` contains a pair of vertices `(ck.1, ck.2)` with `ck.1` in `C`, `ck.2` in `K`, and `ck.1` and `ck.2` adjacent in `G`.
|