SimpleGraph.Subgraph.Connected.mono
theorem SimpleGraph.Subgraph.Connected.mono :
∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph}, H ≤ H' → H.verts = H'.verts → H.Connected → H'.Connected
This theorem states that for any type `V` and a simple graph `G` of that type, if we have two subgraphs `H` and `H'` of `G`, then if `H` is a subgraph of `H'` and the vertices of `H` are the same as the vertices of `H'`, and if `H` is a connected subgraph, then `H'` is also a connected subgraph. In mathematical terms, it says that the connectivity of a subgraph is preserved under taking a supergraph, assuming the vertices remain the same.
More concisely: If `H` is a connected subgraph of simple graph `G` with the same vertices as a larger subgraph `H'` of `G`, then `H'` is also a connected subgraph.
|
SimpleGraph.connected_induce_iff
theorem SimpleGraph.connected_induce_iff :
∀ {V : Type u} {G : SimpleGraph V} {s : Set V}, (SimpleGraph.induce s G).Connected ↔ (⊤.induce s).Connected := by
sorry
This theorem states that for any given type `V`, a simple graph `G` of type `V`, and a set `s` of type `V`, the graph `G` is connected when induced by the set `s` if and only if the induced subgraph of `G` by the set `s` is a connected subgraph of the "top" subgraph of `G`. In other words, restricting the graph `G` to the vertices in set `s` and deleting all edges incident to vertices outside the set `s` will result in a connected graph if and only if the induced subgraph formed by considering `s` as the new vertex set and inducing edges from the original graph `G` also forms a connected subgraph. This theorem shows the equivalence of two different ways of forming subgraphs and their connection properties.
More concisely: A simple graph induced by a set of vertices is connected if and only if the subgraph formed by considering that set as the new vertex set and inducing edges from the original graph is also connected.
|
SimpleGraph.Subgraph.connected_iff'
theorem SimpleGraph.Subgraph.connected_iff' :
∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Connected ↔ H.coe.Connected
This theorem establishes a relationship between a subgraph being connected and the corresponding simple graph, constructed from the vertex set of the subgraph, being connected. Specifically, for any given type of vertices 'V', a simple graph 'G' on 'V', and a subgraph 'H' of 'G', the subgraph 'H' is connected if and only if the simple graph created from the vertex set of the subgraph 'H' is also connected. Here, 'connected' refers to the property of a graph where there exists a path between any two vertices in the graph.
More concisely: A subgraph of a simple graph is connected if and only if the simple subgraph formed by its vertex set is connected.
|
SimpleGraph.Subgraph.Connected.sup
theorem SimpleGraph.Subgraph.Connected.sup :
∀ {V : Type u} {G : SimpleGraph V} {H K : G.Subgraph},
H.Connected → K.Connected → (H ⊓ K).verts.Nonempty → (H ⊔ K).Connected
This theorem is about connected subgraphs in a simple graph. Specifically, it states that for any type `V`, any `SimpleGraph V` denoted as `G`, and any two `SimpleGraph.Subgraph G` denoted as `H` and `K`, if `H` and `K` are both connected and the intersection of their vertices (`H ⊓ K`) is not empty, then the subgraph formed by the union of `H` and `K` (`H ⊔ K`) is also connected. In other words, if two connected subgraphs share at least one vertex, their union will still form a connected subgraph.
More concisely: If two connected subgraphs of a simple graph share at least one vertex, then their union is also a connected subgraph.
|
SimpleGraph.Subgraph.connected_iff
theorem SimpleGraph.Subgraph.connected_iff :
∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph}, H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
This theorem states that for any type `V`, any simple graph `G` of type `V`, and any subgraph `H` of `G`, `H` is connected if and only if `H` is preconnected and the set of vertices of `H` is not empty. A simple graph is said to be connected if there is a path between every pair of distinct vertices, and preconnected if for every pair of vertices, all the vertices between them are also connected. The theorem thus links the concepts of being connected, being preconnected, and having nonempty vertex set in the context of subgraphs of a simple graph.
More concisely: A subgraph of a simple graph is connected if and only if it is preconnected and has a nonempty vertex set.
|