SimpleGraph.adj_iff_exists_edge
theorem SimpleGraph.adj_iff_exists_edge :
∀ {V : Type u} {G : SimpleGraph V} {v w : V}, G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e
This theorem states that in a simple graph, two vertices are considered adjacent if and only if there is an edge between them. The condition `v ≠ w` is necessary to ensure that the two vertices are different endpoints of the edge, because if `v` is equal to `w`, then the existential condition `∃ (e ∈ G.edgeSet), v ∈ e ∧ w ∈ e` would be satisfied by any edge that is incident to `v`.
More concisely: In a simple graph, two vertices are adjacent if and only if there exists an edge connecting them.
|
SimpleGraph.top_adj
theorem SimpleGraph.top_adj : ∀ {V : Type u} (v w : V), ⊤.Adj v w ↔ v ≠ w
This theorem states that for any two vertices 'v' and 'w' of an arbitrary type 'V', they are adjacent in the complete graph (denoted by ⊤) if and only if 'v' is not equal to 'w'. In other words, in a complete graph, any two distinct vertices are connected by an edge.
More concisely: In a complete graph, any two distinct vertices are connected by an edge.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.42
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.42 :
∀ {α : Type u} (x : α) (a b : Set α), (x ∈ a ∩ b) = (x ∈ a ∧ x ∈ b)
This theorem, `Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.42`, is a statement about sets in any type `α`. Given any element `x` of type `α` and any two sets `a` and `b` of type `α`, it states that `x` is an element of the intersection of `a` and `b` if and only if `x` is an element of `a` and `x` is an element of `b`. In other words, the membership of an element in the intersection of two sets is equivalent to the membership of that element in both sets.
More concisely: For any type `α` and sets `a` and `b` in `α`, the element `x` belongs to the intersection `a ∩ b` if and only if `x` belongs to both `a` and `b` (i.e., `x ∈ a` and `x ∈ b`).
|
SimpleGraph.edgeSet_inf
theorem SimpleGraph.edgeSet_inf : ∀ {V : Type u} (G₁ G₂ : SimpleGraph V), (G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet
This theorem states that for any type `V` and any two simple graphs `G₁` and `G₂` defined on that type, the edge set of the intersection of `G₁` and `G₂` is the same as the intersection of the edge sets of `G₁` and `G₂`. In mathematical terms, if we denote by `E(G)` the edge set of a graph `G`, then `E(G₁ ∩ G₂) = E(G₁) ∩ E(G₂)` for any two simple graphs `G₁` and `G₂`.
More concisely: For any type `V` and simple graphs `G₁` and `G₂` on `V`, the edge set of their intersection equals the intersection of their individual edge sets: `E(G₁ ∩ G₂) = E(G₁) ∩ E(G₂)`.
|
SimpleGraph.edgeSet_mono
theorem SimpleGraph.edgeSet_mono : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V}, G₁ ≤ G₂ → G₁.edgeSet ⊆ G₂.edgeSet
This theorem, `SimpleGraph.edgeSet_mono`, is an alias for the reverse direction of `SimpleGraph.edgeSet_subset_edgeSet`. It states that for any two simple graphs `G₁` and `G₂` of vertices `V`, if `G₁` is less than or equal to `G₂` (i.e., the set of edges in `G₁` is a subset of the set of edges in `G₂`), then the edge set of `G₁` is indeed a subset of the edge set of `G₂`.
More concisely: If simple graphs $G\_1$ and $G\_2$ have vertex set $V$ and $G\_1$ is a subgraph of $G\_2$ (i.e., every edge in $G\_1$ is an edge in $G\_2$), then the edge set of $G\_1$ is a subset of the edge set of $G\_2$.
|
SimpleGraph.not_isDiag_of_mem_edgeSet
theorem SimpleGraph.not_isDiag_of_mem_edgeSet :
∀ {V : Type u} (G : SimpleGraph V) {e : Sym2 V}, e ∈ G.edgeSet → ¬e.IsDiag
The theorem `SimpleGraph.not_isDiag_of_mem_edgeSet` states that for any type `V` and a simple graph `G` of that type, if `e` is an element of the edge set of the graph `G`, then `e` cannot be on the diagonal. In other words, an edge of a simple graph cannot connect a vertex to itself.
More concisely: In a simple graph, no edge can connect a vertex to itself.
|
SimpleGraph.edgeSet_sdiff
theorem SimpleGraph.edgeSet_sdiff :
∀ {V : Type u} (G₁ G₂ : SimpleGraph V), (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet
This theorem states that for any two simple graphs, `G₁` and `G₂`, of the same type `V`, the edge set of the graph resulting from the difference of `G₁` and `G₂` (denoted `G₁ \ G₂`) is equal to the difference of the edge sets of `G₁` and `G₂`. That is, subtracting the edges in `G₂` from `G₁` is the same as subtracting the edge set of `G₂` from the edge set of `G₁`.
More concisely: For any simple graphs `G₁` and `G₂` of the same type `V`, the edge difference `(Edge G₁) \ (Edge G₂)` equals the set difference of `Edge G₁` and `Edge G₂`.
|
SimpleGraph.mem_edgeSet
theorem SimpleGraph.mem_edgeSet : ∀ {V : Type u} (G : SimpleGraph V) {v w : V}, s(v, w) ∈ G.edgeSet ↔ G.Adj v w := by
sorry
The theorem `SimpleGraph.mem_edgeSet` states that for any type `V`, any simple graph `G` of type `V`, and any vertices `v` and `w` of type `V`, the pair `(v, w)` is an element of the edge set of `G` if and only if `v` and `w` are adjacent in `G`. In other words, the edge `(v, w)` exists in the graph `G` exactly when `v` and `w` are directly connected by an edge in `G`.
More concisely: For any simple graph G of type V and vertices v, w of type V, (v, w) is in the edge set of G if and only if v and w are adjacent in G.
|
SimpleGraph.incidence_other_prop
theorem SimpleGraph.incidence_other_prop :
∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v),
G.otherVertexOfIncident h ∈ G.neighborSet v
This theorem states that for any given vertex `v` in a simple graph `G` of vertex type `V` where `V` has a decidable equality, and for any edge `e` in the incidence set of `v` (i.e., `e` is an edge incident to `v`), the other vertex of the edge `e` (that is not `v`) is in the neighbor set of `v`. In other words, if an edge is incident to a vertex, the other vertex of that edge is indeed a neighbor of the given vertex.
More concisely: For any simple graph with decidable vertex equality, if vertex `v` has an incident edge `e`, then the vertex at the other end of `e` is in `v`'s neighbor set.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.37
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.37 :
∀ {V : Type u} {v w : V} (s : Set (Sym2 V)), (SimpleGraph.fromEdgeSet s).Adj v w = (s(v, w) ∈ s ∧ v ≠ w)
The theorem, named `Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.37`, states that for any type `V`, any two elements `v` and `w` of type `V`, and any set `s` of unordered pairs from `V`, the adjacency relation in the `SimpleGraph` constructed from the edge set `s` between `v` and `w` is equivalent to the condition that the unordered pair consisting of `v` and `w` is an element of the set `s` and `v` is not equal to `w`. In other words, two vertices `v` and `w` are adjacent in the simple graph derived from the edge set `s` if and only if they form an edge in `s` and they are distinct.
More concisely: In a simple graph with vertex set V and edge set S, vertices v and w are adjacent if and only if {v, w} ∈ S and v ≠ w.
|
SimpleGraph.edgeSet_sdiff_sdiff_isDiag
theorem SimpleGraph.edgeSet_sdiff_sdiff_isDiag :
∀ {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)), G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s
This theorem, named `SimpleGraph.edgeSet_sdiff_sdiff_isDiag`, asserts that for any simple graph `G` of vertices `V` and any set `s` that consists of unordered pairs of vertices (in other words, the edges), the edge set of `G` without the set difference of `s` and the set of diagonal elements `{e | e.IsDiag}` is equal to the edge set of `G` without `s`. In mathematical terms, this is stated as `(G \ from_edgeSet s).edge_set = G.edgeSet \ s`. This theorem is essential in proving the equation `(G \ from_edgeSet s).edge_set = G.edgeSet \ s` using the simplification tactic in Lean 4. Here, "Diag" refers to edges that are loops, i.e., connect a vertex to itself.
More concisely: The theorem asserts that for any simple graph `G` and set `s` of unordered vertex pairs, the edge set difference of `G` with the set difference of `s` and diagonal edges is equal to the edge set difference of `G` with `s`.
|
SimpleGraph.ext
theorem SimpleGraph.ext : ∀ {V : Type u} (x y : SimpleGraph V), x.Adj = y.Adj → x = y
This theorem, `SimpleGraph.ext`, states that for any type `V`, if we have two simple graphs `x` and `y`, and their adjacency relations `x.Adj` and `y.Adj` are the same, then the two simple graphs `x` and `y` are also the same. In the context of graph theory, this means that two simple graphs are considered equal if they have the same set of edges, as the adjacency relation defines the connections between vertices in a graph.
More concisely: If two simple graphs have equal adjacency relations, then they are equal as graphs.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.18
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.18 : ∀ {V : Type u} (v w : V), ⊥.Adj v w = False
This theorem, `Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.18`, states that for any given type `V` and any two instances `v` and `w` of that type, it is not possible for `v` and `w` to be adjacent in the bottom (least) simple graph. In other words, there are no adjacent vertices in the empty simple graph.
More concisely: In the empty simple graph, there are no adjacent vertices.
|
SimpleGraph.edgeSet_strict_mono
theorem SimpleGraph.edgeSet_strict_mono : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V}, G₁ < G₂ → G₁.edgeSet ⊂ G₂.edgeSet
The theorem `SimpleGraph.edgeSet_strict_mono` states that for any two simple graphs `G₁` and `G₂` over the same set of vertices `V`, if `G₁` is strictly smaller than `G₂` (i.e., `G₁` is a proper subgraph of `G₂`), then the set of edges in `G₁` (`G₁.edgeSet`) is a proper subset of the set of edges in `G₂` (`G₂.edgeSet`).
More concisely: If two simple graphs over the same set of vertices have one being a proper subgraph of the other, then the edge set of the smaller graph is a proper subset of the edge set of the larger graph.
|
SimpleGraph.adj_comm
theorem SimpleGraph.adj_comm : ∀ {V : Type u} (G : SimpleGraph V) (u v : V), G.Adj u v ↔ G.Adj v u
This theorem states that for any simple graph `G` with vertex set `V`, the adjacency relation is symmetric. In other words, if vertex `u` is adjacent to vertex `v` in `G`, then it's also the case that `v` is adjacent to `u` in `G`, and vice versa. This captures the intuitive notion of adjacency in an undirected graph, where the order of the vertices does not matter in determining whether a pair of vertices is adjacent or not.
More concisely: For any simple graph `G` with vertex set `V`, if `u` is adjacent to `v` in `G`, then `v` is also adjacent to `u`.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.6
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.6 :
∀ {V : Type u} (G : SimpleGraph V) {v : V}, G.Adj v v = False
This theorem states that for any type `V`, any simple graph `G` of type `SimpleGraph V`, and any vertex `v` of type `V`, the adjacency of `v` to itself in `G` is always `False`. In other words, in a simple graph, no vertex is adjacent to itself.
More concisely: In a simple graph, no vertex is adjacent to itself. (Or, formally in Lean: `∀ (V : Type) (G : SimpleGraph V) (v : V), ¬ Adj G v v`)
|
SimpleGraph.ne_of_adj
theorem SimpleGraph.ne_of_adj : ∀ {V : Type u} (G : SimpleGraph V) {a b : V}, G.Adj a b → a ≠ b
This theorem, `SimpleGraph.ne_of_adj`, states that for any simple graph `G` of type `V`, if two nodes `a` and `b` are adjacent (i.e., `G.Adj a b`), then `a` and `b` must not be identical, denoted by `a ≠ b`. In simpler terms, this theorem ensures that in any simple graph, there are no loops; a node cannot be adjacent to itself.
More concisely: In a simple graph, no node is adjacent to itself.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.10
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.10 :
∀ {V : Type u} (G : SimpleGraph V) (v w : V), Gᶜ.Adj v w = (v ≠ w ∧ ¬G.Adj v w)
The theorem `Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.10` states that for any type `V` and for any simple graph `G` of type `V`, and for any vertices `v` and `w` in this graph, `v` and `w` are adjacent in the complement of `G` if and only if `v` is not equal to `w` and `v` and `w` are not adjacent in `G`. Simply put, it defines the adjacency in the complement graph in terms of the original graph.
More concisely: For any simple graph G and vertices v and w, v and w are adjacent in the complement graph if and only if they are not equal and not adjacent in G.
|
SimpleGraph.Adj.symm
theorem SimpleGraph.Adj.symm : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → G.Adj v u
This theorem, `SimpleGraph.Adj.symm`, states that for any given graph `G` of type `SimpleGraph V`, with `V` being any type, and any two vertices `u` and `v` of `V`, if `u` is adjacent to `v` in `G`, then `v` is also adjacent to `u`. In other words, adjacency in a simple graph is symmetric.
More concisely: If `G` is a simple graph and `u` is adjacent to `v` in `G`, then `v` is adjacent to `u` in `G`.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.23
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.23 :
∀ {V : Type u} (G : SimpleGraph V) {v w : V}, (s(v, w) ∈ G.edgeSet) = G.Adj v w
This theorem states that for any graph `G` of type `SimpleGraph V`, where `V` is any type (representing the vertices), and any two vertices `v` and `w` of this graph, the pair `s(v, w)` (representing an edge) is a member of the edge set of `G`, denoted as `SimpleGraph.edgeSet G`, if and only if `v` and `w` are adjacent in `G`, denoted as `G.Adj v w`. In other words, an edge, represented by the pair of vertices `(v, w)`, exists in the graph `G` if and only if the vertices `v` and `w` are adjacent in `G`.
More concisely: For any simple graph G and vertices v, w of type V, the pair (v, w) is in the edge set of G if and only if v and w are adjacent in G.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.51
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.51 :
∀ {V : Type u} (G : SimpleGraph V) (v w : V), (w ∈ G.neighborSet v) = G.Adj v w
This theorem states that for any given type `V`, a graph `G` of type `SimpleGraph V`, and any two vertices `v` and `w` of type `V`, `w` is in the neighbor set of `v` in `G` if and only if `v` and `w` are adjacent in `G`. In other words, a vertex `w` belongs to the neighbor set of a vertex `v` in a simple graph `G` precisely when there is an edge connecting `v` and `w` in that graph. Therefore, the neighbor set of a vertex in `G` is precisely the set of vertices which are adjacent to it in `G`.
More concisely: In a simple graph, the neighbor set of a vertex equals the set of vertices adjacent to it.
|
SimpleGraph.Adj.ne
theorem SimpleGraph.Adj.ne : ∀ {V : Type u} {G : SimpleGraph V} {a b : V}, G.Adj a b → a ≠ b
This theorem states that for any type `V`, any Simple Graph `G` on `V`, and any two vertices `a` and `b` in `V`, if `a` and `b` are adjacent in `G` (denoted as `G.Adj a b`), then `a` and `b` must not be identical (i.e., `a ≠ b`). In other words, there are no self-loops in a Simple Graph.
More concisely: In a simple graph, no vertex is adjacent to itself.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.61
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.61 :
∀ {V : Type u} (G : SimpleGraph V) (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 given type `V`, any simple graph `G` of vertices of type `V`, any set `s` of unordered pairs of vertices (denoted as `Sym2 V`), and any two vertices `v` and `w` of type `V`, the adjacency relation in the graph obtained by deleting from `G` the edges corresponding to the pairs in `s` between `v` and `w` is equivalent to the condition that `v` and `w` are adjacent in `G` and the pair `(v, w)` is not in the set `s`. In other words, `v` and `w` are connected in the graph after deleting the edges if and only if they were originally connected and their connection was not among those to be removed.
More concisely: For any simple graph `G` of type `V`, vertices `v` and `w` of type `V`, and set `s` of unordered pairs of `V`, the adjacency relation between `v` and `w` in `G` after deleting edges corresponding to pairs in `s` is equivalent to `(v = w) \/ (v, w) IN s ^'` where `s ^'` is the complement of `s`.
|
Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.17
theorem Mathlib.Combinatorics.SimpleGraph.Basic._auxLemma.17 : ∀ {V : Type u} (v w : V), ⊤.Adj v w = (v ≠ w)
This theorem from Mathlib's combinatorics about simple graphs states that for any type `V` and any two elements `v` and `w` of that type, `v` and `w` are adjacent in the complete graph on `V` if and only if `v` is not equal to `w`. In graph theory, a complete graph is a simple undirected graph in which every pair of distinct vertices is connected by a unique edge. Here, ⊤ is used to denote the complete graph.
More concisely: In the complete graph on type `V`, elements `v` and `w` are adjacent if and only if they are distinct.
|
SimpleGraph.edgeSet_fromEdgeSet
theorem SimpleGraph.edgeSet_fromEdgeSet :
∀ {V : Type u} (s : Set (Sym2 V)), (SimpleGraph.fromEdgeSet s).edgeSet = s \ {e | e.IsDiag}
This theorem states that for any set `s` of unordered pairs of type `V`, the edge set for the simple graph constructed from set `s` is equal to the original set `s` excluding any unordered pairs that are on the diagonal. In other words, when a `SimpleGraph` is constructed from a set of edges, all self-loops (edges where both endpoints are the same vertex) are removed, and the remaining set of edges is exactly those from the original set.
More concisely: The set of edges in the simple graph constructed from a set of unordered pairs equals the original set without self-loops (diagonal elements).
|
SimpleGraph.edgeSet_bot
theorem SimpleGraph.edgeSet_bot : ∀ {V : Type u}, ⊥.edgeSet = ∅
This theorem states that for any type `V`, the edge set of the bottom graph (`⊥`) is the empty set (`∅`). In other words, the graph with no vertices and no edges (designated by `⊥`) does not contain any edges in its edge set, hence it is equal to the empty set.
More concisely: The bottom graph (⊥) of any type V has an empty edge set.
|
SimpleGraph.mem_incidence_iff_neighbor
theorem SimpleGraph.mem_incidence_iff_neighbor :
∀ {V : Type u} (G : SimpleGraph V) {v w : V}, s(v, w) ∈ G.incidenceSet v ↔ w ∈ G.neighborSet v
This theorem states that for any simple graph `G` of vertices of type `V` and any two vertices `v` and `w` in the graph, the pair `s(v, w)` (representing an edge) belongs to the incidence set of `v` in `G` if and only if the vertex `w` is in the neighbor set of `v` in `G`. In other words, an edge is incident to a vertex if and only if the other end of the edge is a neighbor of the vertex.
More concisely: For any simple graph G and vertices v, w in G, the edge s(v, w) is in the incidence set of v if and only if w is in the neighbor set of v.
|