Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.21
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.21 : ∀ (p : Prop), (True ∧ p) = p
This theorem, `Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.21`, states that for any proposition `p`, the boolean conjunction (i.e., AND operation) of `True` and `p` is equivalent to `p` itself. In other words, it says if `True` and `p` are both true, then `p` is true - which holds for any proposition `p`. This theorem is fundamental in boolean logic within the Lean Theorem Prover.
More concisely: The theorem asserts that `True` and any proposition `p` are logically equivalent.
|
SimpleGraph.Subgraph.adj_symm
theorem SimpleGraph.Subgraph.adj_symm :
∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) {u v : V}, G'.Adj u v → G'.Adj v u
This theorem states that for any given simple graph `G` with vertices of some type `V` and any subgraph `G'` of this graph, if a vertex `u` is adjacent to a vertex `v` in the subgraph `G'`, then `v` is also adjacent to `u` in `G'`. In other words, the adjacency relationship in the subgraph is symmetric. Any pair of vertices that are connected by an edge in one direction are also connected in the other direction.
More concisely: If `G` is a simple graph and `u` is adjacent to `v` in the subgraph `G'` of `G`, then `v` is adjacent to `u` in `G'`. (Or, symmetrically, if `u` is adjacent to `v` in `G`, then `v` is adjacent to `u` in `G'`. )
|
Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.5
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.5 :
∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v w : V), (w ∈ G'.neighborSet v) = G'.Adj v w
This theorem states that for any type `V`, any simple graph `G` of type `V`, any subgraph `G'` of `G`, and any vertices `v` and `w` of type `V`, `w` is in the neighbor set of `v` in subgraph `G'` if and only if `w` is adjacent to `v` in subgraph `G'`. In other words, a vertex `w` is considered a neighbor of a vertex `v` in a subgraph `G'` of a simple graph `G` exactly when there is an edge connecting them in the subgraph `G'`.
More concisely: In a simple graph `G` of type `V`, a vertex `w` is a neighbor of vertex `v` in subgraph `G'` if and only if there is an edge between `v` and `w` in `G'`.
|
SimpleGraph.Subgraph.induce_mono
theorem SimpleGraph.Subgraph.induce_mono :
∀ {V : Type u} {G : SimpleGraph V} {G' G'' : G.Subgraph} {s s' : Set V},
G' ≤ G'' → s ⊆ s' → G'.induce s ≤ G''.induce s'
This theorem states that for any given type `V` and a simple graph `G` of type `V`, if `G'` and `G''` are subgraphs of `G`, and `s` and `s'` are sets of vertices in `V`, then if `G'` is a subgraph of `G''` and `s` is a subset of `s'`, the induced subgraph of `G'` with vertex set `s` is a subgraph of the induced subgraph of `G''` with vertex set `s'`. In other words, the process of inducing a subgraph preserves the relation of "being a subgraph of".
More concisely: If `G'` is a subgraph of `G''` and `s` is a subset of `s'`, then the induced subgraph of `G'` on `s` is a subgraph of the induced subgraph of `G''` on `s'`.
|
Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.42
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.42 :
∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) (v w : V),
(G'.deleteEdges s).Adj v w = (G'.Adj v w ∧ s(v, w) ∉ s)
This theorem states that for any type `V`, any simple graph `G` of type `V`, any subgraph `G'` of `G`, any set `s` of unordered pairs of vertices, and any two vertices `v` and `w`, the adjacency between `v` and `w` in the subgraph obtained from `G'` by deleting the edges corresponding to the vertex pairs in `s`, equals the statement that `v` and `w` are adjacent in `G'` and the unordered pair `(v, w)` is not in `s`. In other words, after removing specified edges from `G'`, two vertices remain adjacent if and only if they were originally adjacent and their corresponding pair was not included in the set `s` of edges being removed.
More concisely: For any simple graph $G$, subgraph $G'$ with deleted edges $s$, and vertices $v$, $w$, $v$ and $w$ are adjacent in $G'$ if and only if they were adjacent in $G$ and $(v, w) \notin s$.
|
Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.19
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.19 : ∀ {a b c : Prop}, (a ∧ b → c) = (a → b → c) := by
sorry
This theorem, `Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.19`, states that for any three propositions `a`, `b`, and `c`, the proposition "`a` and `b` imply `c`" is equivalent to the proposition "`a` implies that `b` implies `c`". In other words, if `a` and `b` are true, then `c` must also be true; this is the same as stating that if `a` is true, then if `b` is also true, `c` must be true. This captures a fundamental property of logical implication.
More concisely: The theorem `Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.19` in Lean 4 states that the implications `(a ⟹ b) ⟹ c` and `a ⟹ (b ⟹ c)` are logically equivalent.
|
SimpleGraph.Subgraph.le_induce_union
theorem SimpleGraph.Subgraph.le_induce_union :
∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s s' : Set V},
G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s')
This theorem states that for any type `V`, any `SimpleGraph` `G` of `V`, any subgraph `G'` of `G`, and any two sets `s` and `s'` of `V`, the union of the induced subgraphs of `G'` with respect to `s` and `s'` is contained within (or equal to) the induced subgraph of `G'` with respect to the union of `s` and `s'`. In other words, if we induce a subgraph from `s` and another from `s'`, then their union is a subgraph of the induced subgraph from `s ∪ s'`.
More concisely: For any simple graph `G` on type `V`, any subgraph `G'` of `G`, and any sets `s` and `s'` of `V`, the induced subgraph of `G'` on `s ∪ s'` is contained in the union of the induced subgraphs of `G'` on `s` and `s'`.
|
Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.6
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.6 :
∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v w : V}, (s(v, w) ∈ G'.edgeSet) = G'.Adj v w
This theorem states that for any simple graph `G` with vertices of some type `V`, and any subgraph `G'` of `G`, and any pair of vertices `v` and `w` from `V`, the pair `(v, w)` is in the edge set of the subgraph `G'` if and only if vertices `v` and `w` are adjacent in the subgraph `G'`. In other words, it forms a connection between the edge set of a subgraph and the adjacency relationship in that subgraph.
More concisely: For any simple graph G and its subgraph G', vertices v and w are in the edge set of G' if and only if they are adjacent in G'.
|
SimpleGraph.Subgraph.ext
theorem SimpleGraph.Subgraph.ext :
∀ {V : Type u} {G : SimpleGraph V} (x y : G.Subgraph), x.verts = y.verts → x.Adj = y.Adj → x = y
This theorem states that for any type `V` and any simple graph `G` of type `SimpleGraph V`, if we have two subgraphs `x` and `y` of `G`, and if the vertices `x.verts` of `x` are equal to the vertices `y.verts` of `y`, and also the adjacency relation `x.Adj` of `x` is equal to the adjacency relation `y.Adj` of `y`, then the two subgraphs `x` and `y` are in fact the same subgraph. In other words, two subgraphs are considered equal if they have the same vertices and the same adjacency relation.
More concisely: given types `V` and a simple graph `G` of type `SimpleGraph V`, if `x` and `y` are subgraphs of `G` with equal vertices and identical adjacency relations, then `x = y`.
|
Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.10
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.10 :
∀ {V : Type u} {G : SimpleGraph V} {a b : V}, ⊤.Adj a b = G.Adj a b
This theorem from the Mathlib library in Lean 4 states that for any type `V`, any simple graph `G` of vertices of type `V`, and any two vertices `a` and `b` of that type, the adjacency of `a` and `b` in the topmost, or complete, subgraph (represented by `⊤`) is equal to the adjacency of `a` and `b` in the original graph `G`. In other words, `a` and `b` are adjacent in the complete subgraph if and only if they are adjacent in `G`.
More concisely: For any simple graph `G` and vertices `a` and `b` of type `V` in `G`, `a` and `b` are adjacent in the complete subgraph `⊤` if and only if they are adjacent in `G`.
|
Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.13
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.13 :
∀ {V : Type u} {G : SimpleGraph V} {a b : V} {s : Set G.Subgraph},
(sInf s).Adj a b = ((∀ G' ∈ s, G'.Adj a b) ∧ G.Adj a b)
This theorem, `Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.13`, states that for any type `V`, a simple graph `G` of type `V`, and any two vertices `a` and `b` from `V`, along with a set `s` of subgraphs of `G`, the adjacency in the infimum of `s` between vertices `a` and `b` is equal to the conjunction of the adjacency in all subgraphs `G'` in `s` between `a` and `b`, and the adjacency in graph `G` between `a` and `b`. In simpler terms, two vertices `a` and `b` are considered adjacent in the infimum of a set of subgraphs of `G` if and only if they are adjacent in every subgraph within the set and also in the original graph `G`.
More concisely: The adjacency relation in the infimum of a set of subgraphs of a simple graph is the conjunction of the adjacency relations in each subgraph and the graph itself.
|
Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.23
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.23 :
∀ {V : Type u} {G : SimpleGraph V} (v : V) (H : G.Subgraph), (G.singletonSubgraph v ≤ H) = (v ∈ H.verts)
This theorem states that for any type `V`, any simple graph `G` of type `V`, any vertex `v` of type `V`, and any subgraph `H` of `G`, the singleton subgraph of `G` containing only the vertex `v` is a subgraph of `H` if and only if `v` is a vertex in `H`. In other words, it defines the condition for a one-vertex subgraph to be a subgraph of another given subgraph.
More concisely: For any simple graph G of type V, vertex v of type V, and subgraph H of G, the singleton subgraph of G containing only vertex v is a subgraph of H if and only if v is a vertex in H.
|
SimpleGraph.Subgraph.Adj.symm
theorem SimpleGraph.Subgraph.Adj.symm :
∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {u v : V}, G'.Adj u v → G'.Adj v u
The theorem `SimpleGraph.Subgraph.Adj.symm` states that for any type `V`, given a simple graph `G` of vertices of type `V`, a subgraph `G'` of `G`, and vertices `u` and `v`, if `u` is adjacent to `v` in the subgraph `G'`, then `v` is also adjacent to `u` in the same subgraph. In other words, the adjacency relationship in a subgraph of a simple graph is symmetric.
More concisely: If `G` is a simple graph and `u`, `v` are vertices in a subgraph `G'` of `G` such that `u` is adjacent to `v` in `G'`, then `v` is adjacent to `u` in `G'`.
|
Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.12
theorem Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.12 :
∀ {V : Type u} {G : SimpleGraph V} {a b : V} {s : Set G.Subgraph}, (sSup s).Adj a b = ∃ G_1 ∈ s, G_1.Adj a b := by
sorry
This theorem, `Mathlib.Combinatorics.SimpleGraph.Subgraph._auxLemma.12`, states that for any type `V`, any Simple Graph `G` of type `V`, and any two vertices `a` and `b` of type `V`, and for any set `s` of subgraphs of `G`, the adjacency of `a` and `b` in the supergraph of `s` is equivalent to the existence of a subgraph `G_1` in `s` where `a` and `b` are adjacent. In other words, two vertices are adjacent in the supergraph if and only if there exists a subgraph within the set where those two vertices are also adjacent.
More concisely: For any simple graph G, vertices a and b are adjacent in the supergraph of a set S of subgraphs if and only if there exists a subgraph in S with a and b as adjacent vertices.
|