SimpleGraph.Walk.exists_concat_eq_cons
theorem SimpleGraph.Walk.exists_concat_eq_cons :
∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w),
∃ x, ∃ (h' : G.Adj u x), ∃ q, p.concat h = SimpleGraph.Walk.cons h' q
This theorem states that for any simple graph `G` with vertices of type `V`, and any `u`, `v`, and `w` vertices, if there exists a walk `p` from `u` to `v`, and `v` is adjacent to `w`, then there exists a vertex `x` such that `u` is adjacent to `x`, and there exists a walk `q` such that concatenating the walk `p` with the edge going from `v` to `w` is equivalent to adding the edge going from `u` to `x` at the beginning of the walk `q`. In other words, non-trivial concatenations in a graph walk can always be represented as cons operations which prepends an edge to a walk.
More concisely: For any simple graph and vertices `u`, `v`, `w` where `u` is adjacent to `x` via a walk `p` and `v` is adjacent to `w`, there exists a walk `q` such that the concatenation of the edges `(u, x)` and `(v, w)` is equivalent to the walk obtained by prepending the edge `(u, x)` to `q`.
|
Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.6
theorem Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.6 :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), (p.support = []) = False
This theorem states that for any SimpleGraph `G` with vertices of type `V`, and any two vertices `u` and `v` in `G`, if there exists a walk `p` from `u` to `v`, then `u` is always an element of the support of `p`. The support of a walk is the list of vertices the walk visits in order.
More concisely: For any SimpleGraph `G` and vertices `u` and `v` in `G`, if there exists a walk from `u` to `v`, then `u` is in the support of that walk.
|
SimpleGraph.Walk.map_isTrail_of_injective
theorem SimpleGraph.Walk.map_isTrail_of_injective :
∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G.Hom G'} {u v : V} {p : G.Walk u v},
Function.Injective ⇑f → p.IsTrail → (SimpleGraph.Walk.map f p).IsTrail
This theorem, referred to as `SimpleGraph.Walk.map_isTrail_of_injective`, states that for all types `V` and `V'`, all simple graphs `G` on `V` and `G'` on `V'`, all graph homomorphisms `f` from `G` to `G'`, all vertices `u` and `v` in `V`, and all walks `p` from `u` to `v` in `G`, if the function `f` is injective (meaning that if `f x = f y` then `x = y`) and the walk `p` is a trail (meaning that all edges in the walk are distinct), then the mapped walk `(SimpleGraph.Walk.map f p)` in the graph `G'` is also a trail.
More concisely: If `f` is an injective graph homomorphism from simple graph `G` to simple graph `G'`, and walk `p` in `G` is a trail, then `(SimpleGraph.Walk.map f p)` is a trail in `G'`.
|
SimpleGraph.Walk.reachable
theorem SimpleGraph.Walk.reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Walk u v → G.Reachable u v := by
sorry
This theorem states that for any given type `V`, any Simple Graph `G` of type `V`, and any two vertices `u` and `v` of type `V`, if there is a walk from vertex `u` to vertex `v` in the graph `G`, then the vertices `u` and `v` are reachable. In other words, the existence of a walk between two vertices in a simple graph implies that these two vertices are reachable from each other.
More concisely: In a simple graph, the existence of a walk between two vertices implies their reachability.
|
Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.20
theorem Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.20 :
∀ {α : Type u_1} {a b : α} {l : List α}, (a ∈ b :: l) = (a = b ∨ a ∈ l)
This theorem states that for any type `α`, an element `a` of that type, and a list `l` of elements of the same type, the assertion that the list `l` prefixed with `a` (i.e., `a :: l`) has no duplicate elements (formally, `List.Nodup (a :: l)`) is equivalent to the conjunction of the statements that `a` does not belong to `l` (formally, `a ∉ l`) and that `l` itself has no duplicate elements (formally, `List.Nodup l`).
More concisely: For any type `α` and list `l` of elements of type `α`, the list `a :: l` has no duplicate elements if and only if `a` is not in `l` and `l` itself has no duplicate elements.
|
SimpleGraph.ConnectedComponent.ind₂
theorem SimpleGraph.ConnectedComponent.ind₂ :
∀ {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → G.ConnectedComponent → Prop},
(∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)) → ∀ (c d : G.ConnectedComponent), β c d
The theorem `SimpleGraph.ConnectedComponent.ind₂` states that for any type `V` and any simple graph `G` on `V`, if for a property `β`, which is a relation between connected components of `G`, we have that this property holds for all pairs of vertices `v` and `w` in `V` when considered as their respective connected components via `SimpleGraph.connectedComponentMk`, then this property `β` also holds for any two arbitrary connected components `c` and `d` of `G`. In other words, if a property holds for all pairs of vertices considered as connected components, then it holds for all pairs of connected components.
More concisely: If a property holds between connected components of a simple graph, given that it holds between any pair of vertices in their respective connected components, then the property holds between any two connected components.
|
SimpleGraph.Walk.map_eq_of_eq
theorem SimpleGraph.Walk.map_eq_of_eq :
∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (p : G.Walk u v) {f : G.Hom G'}
(f' : G.Hom G') (h : f = f'), SimpleGraph.Walk.map f p = (SimpleGraph.Walk.map f' p).copy ⋯ ⋯
This theorem states that for any types `V` and `V'`, any simple graphs `G` and `G'` on `V` and `V'` respectively, any vertices `u` and `v` of `G`, and any walk `p` from `u` to `v` in `G`, if `f` and `f'` are graph homomorphisms from `G` to `G'` such that `f` is equal to `f'`, then the walk obtained by mapping `p` via `f` is equivalent to the walk obtained by mapping `p` via `f'`.
This is to say, if two graph homomorphisms are equal, then the walks produced by applying these homomorphisms to a given walk are also equal. This is particularly important in the context of graphs, where equality of vertices is a crucial concept, necessitating the need to work with equality of graph homomorphisms as well.
More concisely: If two graph homomorphisms between simple graphs with equal domains are equal, then they map equal walks to equal walks.
|
SimpleGraph.Reachable.refl
theorem SimpleGraph.Reachable.refl : ∀ {V : Type u} {G : SimpleGraph V} (u : V), G.Reachable u u
This theorem states that for any type `V` and any simple graph `G` with vertices of type `V`, every vertex `u` in `G` is reachable from itself. In other words, there exists a walk (possibly empty) in graph `G` that starts and ends at the same vertex `u`. This is an aspect of the reflexivity property in reachability in graphs.
More concisely: For any simple graph `G` with vertices of type `V`, every vertex `u` in `G` is reachable from itself. Equivalently, there exists a walk of length 0 or more in `G` starting and ending at any vertex `u`.
|
SimpleGraph.Walk.verts_toSubgraph
theorem SimpleGraph.Walk.verts_toSubgraph :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.toSubgraph.verts = {w | w ∈ p.support}
This theorem states that for any type `V`, any simple graph `G` of type `V`, and any two vertices `u` and `v` of type `V`, for any walk `p` from `u` to `v` in graph `G`, the set of vertices of the subgraph generated by the walk `p` is exactly the set of vertices that the walk `p` visits in order. In other words, when you take a walk `p` in a graph `G`, and then consider the subgraph of `G` that includes just the vertices and edges involved in that walk, the vertices of this subgraph are precisely the ones that appear in the support of the walk `p`.
More concisely: For any simple graph `G` and walk `p` in `G`, the subgraph generated by `p` consists exactly of the vertices visited in order by `p`.
|
SimpleGraph.Reachable.map
theorem SimpleGraph.Reachable.map :
∀ {V : Type u} {V' : Type v} {u v : V} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G.Hom G'),
G.Reachable u v → G'.Reachable (f u) (f v)
The theorem `SimpleGraph.Reachable.map` states that for any two types `V` and `V'`, for any vertices `u` and `v` of type `V`, for any simple graphs `G` and `G'` of type `V` and `V'` respectively, and for a function `f` that maps from `G` to `G'`, if `u` and `v` are reachable in the graph `G`, then the images of `u` and `v` under the function `f` are reachable in the graph `G'`. In other words, the reachability relation is preserved under the map from `G` to `G'`.
More concisely: If `G` is a simple graph and `f` is a function from the vertices of `G` to the vertices of a simple graph `G'`, then for any vertices `u` and `v` of `G` such that there is a path from `u` to `v` in `G`, there is a path from `f(u)` to `f(v)` in `G'`.
|
Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.29
theorem Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.29 :
∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.IsTrail = True
This theorem, `Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.29`, states that for any given simple graph `G` with vertex type `V`, and any two vertices `u` and `v` in this graph, a walk `p` from `u` to `v` is a trail if and only if the list of edges visited by this walk, `SimpleGraph.Walk.edges p`, has no duplicates (`List.Nodup`).
In more detail, a "trail" in graph theory is a walk that does not repeat any edges. Here, the theorem is relating this concept to the function `List.Nodup`, which checks if a list has no repeated elements. Thus, the theorem's statement can be summarized as "in a simple graph, a walk is a trail if the list of its visited edges has no duplications."
More concisely: A walk in a simple graph is a trail if and only if the list of its edges contains no duplicates.
|
SimpleGraph.Walk.fst_mem_support_of_mem_edges
theorem SimpleGraph.Walk.fst_mem_support_of_mem_edges :
∀ {V : Type u} {G : SimpleGraph V} {t u v w : V} (p : G.Walk v w), s(t, u) ∈ p.edges → t ∈ p.support
The theorem `SimpleGraph.Walk.fst_mem_support_of_mem_edges` states that, for any type `V`, any simple graph `G` of type `V`, and any vertices `t`, `u`, `v`, `w` of type `V`, if a walk `p` exists in the graph `G` from `v` to `w`, and the edge `(t, u)` is in the list of edges visited by the walk `p`, then the vertex `t` is in the list of vertices visited by the walk `p`. In other words, if a particular edge is visited during a walk, then the first vertex of that edge is definitely visited during the walk.
More concisely: If a simple graph walk visits an edge (t, u), then the vertex t is in the visited set of the walk.
|
SimpleGraph.Walk.toDeleteEdges.proof_1
theorem SimpleGraph.Walk.toDeleteEdges.proof_1 :
∀ {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)) {v w : V} (p : G.Walk v w),
(∀ e ∈ p.edges, e ∉ s) → ∀ e ∈ p.edges, e ∈ (G.deleteEdges s).edgeSet
This theorem states that for any type `V`, any simple graph `G` of vertex type `V`, any set `s` of unordered pairs of vertices, and any walk `p` in `G` from vertex `v` to vertex `w`, if all edges in the walk `p` do not fall within the set `s`, then all edges in the walk `p` are present in the edge set of the graph obtained by deleting edges in `G` that correspond to the unordered pairs in `s`. In other words, if `p` is a walk in `G` whose edges are not in `s`, then `p` remains a walk in `G` after deletion of the edges specified by `s`.
More concisely: For any simple graph `G` of type `V` and any walk `p` in `G` from vertex `v` to vertex `w` whose edges are not in the set `s` of unordered edge pairs, all edges in `p` are in the edge set of the graph obtained by deleting edges corresponding to `s`.
|
SimpleGraph.Walk.take_spec
theorem SimpleGraph.Walk.take_spec :
∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support),
(p.takeUntil u h).append (p.dropUntil u h) = p
The `SimpleGraph.Walk.take_spec` theorem states that for any type `V`, any simple graph `G` on `V`, any vertices `u`, `v`, `w` of `V`, and any walk `p` from `v` to `w` in `G`, if `u` is a vertex in the support of the walk `p`, then appending the walk from the start of `p` until `u` (`SimpleGraph.Walk.takeUntil p u h`) to the walk from `u` until the end of `p` (`SimpleGraph.Walk.dropUntil p u h`) yields the original walk `p`. This theorem essentially asserts that `takeUntil` and `dropUntil` functions partition the walk into two segments at the vertex `u` in such a way that concatenating these segments reconstructs the original walk.
More concisely: For any simple graph `G`, vertices `u`, `v`, `w`, and walk `p` from `v` to `w` in `G`, if `u` is on `p`, then `p` is the concatenation of the sub-walk from `v` to `u` and the sub-walk from `u` to `w`.
|
SimpleGraph.Walk.reverse_append
theorem SimpleGraph.Walk.reverse_append :
∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w),
(p.append q).reverse = q.reverse.append p.reverse
The theorem `SimpleGraph.Walk.reverse_append` states that for any type `V`, any simple graph `G` of type `V`, and any vertices `u`, `v`, `w` of type `V`, if there is a walk `p` from `u` to `v` and a walk `q` from `v` to `w` in the graph `G`, then reversing the walk that is the append of `p` and `q` is the same as appending the reverse of `q` and the reverse of `p`. In simpler terms, if you reverse a path made by appending two walks, it's the same as appending the reverses of the original walks, but in the opposite order.
More concisely: For any simple graph `G` and vertices `u`, `v`, `w` in its type `V`, if there exist walks `p` from `u` to `v` and `q` from `v` to `w`, then the walk obtained by reversing `p` and appending it to the reversed `q` is equal to the walk obtained by reversing `q` and appending it to the reversed `p`.
|
SimpleGraph.Walk.edges_subset_edgeSet
theorem SimpleGraph.Walk.edges_subset_edgeSet :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) ⦃e : Sym2 V⦄, e ∈ p.edges → e ∈ G.edgeSet
This theorem states that every edge in the list of edges visited in order by a walk on a simple graph is an actual edge of the graph. In other words, for any walk `p` from vertex `u` to vertex `v` on a simple graph `G` of vertices of type `V`, and for any edge `e` represented as an unordered pair of vertices, if `e` is in the list of edges traversed by `walk p`, then `e` is in the set of edges of `G`. This essentially asserts that a walk on a graph cannot include edges that are not present in the graph itself.
More concisely: For any simple graph $G$ and walk $p$ from vertex $u$ to vertex $v$, every edge in the traversed by the walk belongs to the graph $G$.
|
SimpleGraph.Walk.transfer.proof_4
theorem SimpleGraph.Walk.transfer.proof_4 :
∀ {V : Type u_1} {G : SimpleGraph V} (H : SimpleGraph V) (u w v : V) (h : G.Adj u v) (p : G.Walk v w),
(∀ e ∈ (SimpleGraph.Walk.cons' u v w h p).edges, e ∈ H.edgeSet) → ∀ e ∈ p.edges, e ∈ H.edgeSet
The theorem `SimpleGraph.Walk.transfer.proof_4` states that for any type `V` and any simple graphs `G` and `H` with vertices `u`, `w`, and `v`, if `u` is adjacent to `v` in `G` and there is a walk `p` from `v` to `w` in `G`, then if all edges in the walk from `u` to `w` (which is made by concatenating the edge from `u` to `v` and the walk `p`) are in the edge set of `H`, then all edges in the walk `p` must also be in the edge set of `H`. In other words, if every edge in the extended walk is in `H`, then every edge in the original walk is also in `H`.
More concisely: If a simple graph `H` contains every edge in the path connecting vertices `u` and `w` in a simple graph `G`, then every edge in the path between `u` and `w` in `G` is also in `H`.
|
SimpleGraph.Walk.exists_cons_eq_concat
theorem SimpleGraph.Walk.exists_cons_eq_concat :
∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
∃ x q, ∃ (h' : G.Adj x w), SimpleGraph.Walk.cons h p = q.concat h'
This theorem states that in a Simple Graph, any non-trivial walk starting with a `cons` operation (i.e., appending an edge and a vertex to the beginning of a walk) can be represented as a `concat` walk (i.e., appending an edge and a vertex to the end of a walk). Given a Simple Graph `G` with vertices `u`, `v`, and `w` such that `u` is adjacent to `v`, and a walk `p` from `v` to `w`, there exist a vertex `x` and a walk `q` such that `x` is adjacent to `w` and the `cons` walk from `u` to `w` via `p` equals the `concat` walk from `u` to `w` via `q`.
More concisely: In a Simple Graph, any non-trivial walk starting with a cons operation can be equivalently represented as a concat walk by introducing an intermediate vertex.
|
SimpleGraph.Walk.map_isTrail_iff_of_injective
theorem SimpleGraph.Walk.map_isTrail_iff_of_injective :
∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G.Hom G'} {u v : V} {p : G.Walk u v},
Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsTrail ↔ p.IsTrail)
The theorem `SimpleGraph.Walk.map_isTrail_iff_of_injective` states that for any types `V` and `V'`, any simple graphs `G` and `G'` on `V` and `V'` respectively, any graph homomorphism `f` from `G` to `G'`, and any vertices `u` and `v` in `G`, if `f` is an injective function, then a walk `p` from `u` to `v` in `G` is a trail if and only if the mapped walk in `G'` is also a trail. A trail in a graph is a walk in which no edge is repeated. Graph homomorphisms map vertices to vertices and edges to edges, preserving the edge-vertex incidence relation.
More concisely: Given simple graphs G and G' with graph homomorphism f, injectivity of f implies that a walk in G is a trail if and only if its image under f is a trail in G'.
|
SimpleGraph.Walk.map_isCycle_iff_of_injective
theorem SimpleGraph.Walk.map_isCycle_iff_of_injective :
∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G.Hom G'} {u : V} {p : G.Walk u u},
Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsCycle ↔ p.IsCycle)
This theorem states that for all types `V` and `V'` with corresponding simple graphs `G` and `G'`, and a graph homomorphism `f` from `G` to `G'`, if `f` is injective then a walk `p` starting and ending at a vertex `u` in `G` is a cycle if and only if the corresponding walk `SimpleGraph.Walk.map f p` in `G'` is a cycle. In other words, the property of being a cycle is preserved under the action of an injective map from one graph to another.
More concisely: If `f` is an injective graph homomorphism from simple graph `G` to simple graph `G'`, then a walk in `G` starting and ending at vertex `u` forms a cycle if and only if the image walk in `G'` formed by applying `f` to each vertex and edge of the walk also forms a cycle.
|
SimpleGraph.Adj.reachable
theorem SimpleGraph.Adj.reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → G.Reachable u v := by
sorry
This theorem states that for any type `V`, any simple graph `G` of type `V`, and any two vertices `u` and `v` of type `V`, if `u` and `v` are adjacent in the graph `G` (denoted by `G.Adj u v`), then `u` and `v` are reachable from each other in the graph `G`. In other words, there exists a walk in the graph `G` that starts at vertex `u` and ends at vertex `v`.
More concisely: For any simple graph `G` and vertices `u` and `v` in its type `V`, if `u` is adjacent to `v` in `G` (`G.Adj u v`), then there exists a walk from `u` to `v` in `G`.
|
Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.58
theorem Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.58 :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk v u) (h : G.Adj u v),
(SimpleGraph.Walk.cons h p).IsCycle = (p.IsPath ∧ s(u, v) ∉ p.edges)
This theorem states that for any type `V` and for any `SimpleGraph G` of vertices of type `V`, and for any two vertices `v` and `w` of this graph, the connected components of `v` and `w` in `G` are the same if and only if `v` and `w` are reachable from each other in `G`. In mathematical terms, two vertices `v` and `w` are said to be reachable from each other in a graph if there exists a walk (a sequence of vertices and edges) from `v` to `w`. The connected component of a vertex in a graph is the subgraph consisting of the vertex and all vertices reachable from it. Therefore, the theorem essentially establishes a connection between the notion of reachable vertices and connected components in a graph.
More concisely: Two vertices in a simple graph are in the same connected component if and only if they are reachable from each other.
|
SimpleGraph.Reachable.elim
theorem SimpleGraph.Reachable.elim :
∀ {V : Type u} {G : SimpleGraph V} {p : Prop} {u v : V}, G.Reachable u v → (G.Walk u v → p) → p
This theorem states that for any type `V`, any simple graph `G` of type `V`, any proposition `p`, and any vertices `u` and `v` of type `V`, if `u` and `v` are reachable in graph `G` (i.e., there exists a walk from `u` to `v` in the graph), then if the existence of a walk from `u` to `v` implies the truth of proposition `p`, it follows that `p` is true. In simpler terms, it allows us to make inferences about a property `p` given the condition that there is a walk between two vertices in a simple graph.
More concisely: If in a simple graph, there is a walk between vertices `u` and `v`, and the proposition `p` holds along every walk from `u` to `v`, then `p` is true for `v`.
|
SimpleGraph.Walk.reverseAux_append
theorem SimpleGraph.Walk.reverseAux_append :
∀ {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (q : G.Walk u w) (r : G.Walk w x),
(p.reverseAux q).append r = p.reverseAux (q.append r)
This theorem, `SimpleGraph.Walk.reverseAux_append`, states that given a simple graph `G` over vertices of type `V` and three walks `p`, `q`, and `r` in `G` such that `p` is a walk from `u` to `v`, `q` is a walk from `u` to `w`, and `r` is a walk from `w` to `x`, the operation of appending the walk `r` to the reversed walk obtained by applying the `reverseAux` function to `p` and `q` is equivalent to the reversed walk obtained by applying the `reverseAux` function to `p` and the appended walk of `q` and `r`. In simpler terms, the theorem deals with the commutativity of reversing and appending walks in a graph.
More concisely: Given a simple graph and walks `p` from `u` to `v`, `q` from `u` to `w`, and `r` from `w` to `x`, the reversed walks obtained by appending `r` to `reverseAux(p, q)` and applying `reverseAux` to `p` and appending `q` and `r` are equal.
|
SimpleGraph.Reachable.symm
theorem SimpleGraph.Reachable.symm : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Reachable u v → G.Reachable v u
The theorem `SimpleGraph.Reachable.symm` states that for any vertices `u` and `v` of a given simple graph `G`, if `u` is reachable from `v`, then `v` is also reachable from `u`. In other words, the reachability relation in a simple graph is symmetric.
More concisely: If vertices `u` and `v` in a simple graph are reachable from each other, then they are mutually reachable.
|
SimpleGraph.Walk.darts_reverse
theorem SimpleGraph.Walk.darts_reverse :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v),
p.reverse.darts = (List.map SimpleGraph.Dart.symm p.darts).reverse
This theorem states that for any simple graph `G` and any two vertices `u` and `v` in the graph, if there is a walk `p` from `u` to `v`, then the list of "darts" (i.e., edges) visited in the reverse walk from `v` to `u` is equivalent to the list of the darts visited in the original walk `p` but with their orientation reversed and listed in reverse order. Specifically, each dart in the reverse walk corresponds to the "symm" (i.e., the opposite orientation) of a dart in the original walk, and the sequence of darts in the reverse walk follows the reverse of the sequence in the original walk.
More concisely: For any simple graph and vertices u, v connected by a walk, the list of reversed and oppositely oriented darts along the reverse walk from v to u is equivalent to the list of darts along the original walk from u to v.
|
SimpleGraph.Walk.IsTrail.mapLe
theorem SimpleGraph.Walk.IsTrail.mapLe :
∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
p.IsTrail → (SimpleGraph.Walk.mapLe h p).IsTrail
This theorem, referred to as **Alias** of the reverse direction of `SimpleGraph.Walk.mapLe_isTrail`, states that for any types `V`, any simple graphs `G` and `G'` on `V`, any vertices `u` and `v` in `V`, and any walk `p` from `u` to `v` in `G`, if `G` is a subgraph of `G'` (denoted by `G ≤ G'`) and `p` is a trail in `G`, then the walk `p` mapped to the supergraph `G'` (denoted by `SimpleGraph.Walk.mapLe h p`) is also a trail in `G'`.
In other words, if a walk in a graph is a trail (i.e., does not repeat any edges), mapping this walk to a supergraph of the original graph also results in a trail.
More concisely: If `G ≤ G'`, `u` and `v` are vertices in a simple graph `G`, `p` is a trail from `u` to `v` in `G`, then `SimpleGraph.Walk.mapLe h p` is a trail in `G'`.
|
SimpleGraph.Walk.exists_boundary_dart
theorem SimpleGraph.Walk.exists_boundary_dart :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (S : Set V),
u ∈ S → v ∉ S → ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
This theorem states that for any graph `G` of some vertex type `V`, if we have a walk `p` from one vertex `u` to another vertex `v` such that `u` belongs to a set `S`, but `v` does not belong to `S`, then there exists a dart (an edge directed from one vertex to another) in the walk such that the start vertex of the dart is in the set `S` but the end vertex is not in `S`. This dart thus lies on the "boundary" of the set `S` in the context of the walk from `u` to `v`.
More concisely: In any graph, if there's a walk from a vertex in a set to a vertex not in that set, then the walk contains an edge with one end in the set and the other end outside it.
|
SimpleGraph.Walk.map_isCycle_of_injective
theorem SimpleGraph.Walk.map_isCycle_of_injective :
∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G.Hom G'} {u : V} {p : G.Walk u u},
Function.Injective ⇑f → p.IsCycle → (SimpleGraph.Walk.map f p).IsCycle
This theorem, `SimpleGraph.Walk.map_isCycle_of_injective`, states that for all types `V` and `V'`, for any simple graphs `G` and `G'` on `V` and `V'` respectively, and any graph homomorphism `f` from `G` to `G'`, as well as for any vertex `u` in `V` and a walk `p` from `u` to `u` in `G`, if `f` is injective, and `p` is a cycle in `G`, then the walk `p` mapped by `f` to `G'` is also a cycle in `G'`. Here, a function is injective if for every pair of inputs that the function maps to equal outputs, those inputs were actually the same. A walk in a graph is a cycle if it starts and ends at the same vertex, and does not repeat any edge.
More concisely: If `f` is an injective graph homomorphism from simple graphs `G` to `G'`, and `p` is a cycle in `G`, then the image of `p` under `f` is also a cycle in `G'`.
|
SimpleGraph.connected_iff
theorem SimpleGraph.connected_iff : ∀ {V : Type u} (G : SimpleGraph V), G.Connected ↔ G.Preconnected ∧ Nonempty V := by
sorry
The theorem `SimpleGraph.connected_iff` states that, for any type `V` and a Simple Graph `G` on that type, `G` is connected if and only if `G` is preconnected and `V` is not empty. In terms of graph theory, a graph is considered connected if there exists a path between every pair of vertices. In this context, preconnected means that for every pair of vertices in the graph, it is possible to reach one from the other, and `Nonempty V` asserts that there exists at least one vertex in the graph.
More concisely: A Simple Graph on a non-empty type is connected if and only if it is preconnected.
|
SimpleGraph.Walk.IsTrail.of_mapLe
theorem SimpleGraph.Walk.IsTrail.of_mapLe :
∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
(SimpleGraph.Walk.mapLe h p).IsTrail → p.IsTrail
This theorem, `SimpleGraph.Walk.IsTrail.of_mapLe`, states that for any types `V` and any two simple graphs `G` and `G'` on `V`, if `G` is a subgraph of `G'` (expressed as `G ≤ G'`), and for any two vertices `u` and `v` in `V`, if a walk `p` from `u` to `v` in the supergraph `G'` is a trail (i.e., a walk with no repeated edges), then the corresponding walk in the subgraph `G` is also a trail. In other words, a trail in a supergraph remains a trail when mapped to its subgraph.
More concisely: If `G` is a subgraph of `G'` and `p` is a trail in `G'`, then `p` restricted to edges in `G` is a trail in `G`.
|
Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.7
theorem Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.7 :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), (u ∈ p.support) = True
This theorem states that, for any type `V`, any simple graph `G` of type `V`, and any two vertices `u` and `v` of type `V`, if there exists a walk `p` from `u` to `v` in graph `G`, then vertex `v` is always included in the support list of walk `p`. The support of a walk is defined as the list of vertices it visits in order. Therefore, the theorem asserts that the terminal vertex of a walk is always a part of the vertices visited in the walk.
More concisely: For any simple graph and any two vertices, if there is a walk connecting them, then the terminal vertex is in the support of that walk.
|
SimpleGraph.Walk.IsCycle.mapLe
theorem SimpleGraph.Walk.IsCycle.mapLe :
∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
p.IsCycle → (SimpleGraph.Walk.mapLe h p).IsCycle
This theorem, `SimpleGraph.Walk.IsCycle.mapLe`, states that for any type `V` and any two simple graphs `G` and `G'` over this type, if `G` is a subgraph of `G'` (denoted by `G ≤ G'`), and for any vertex `u` in `V` if there is a closed walk `p` in `G` starting and ending at `u` forming a cycle (`p.IsCycle`), then the corresponding walk in `G'` obtained by mapping `p` via `SimpleGraph.Walk.mapLe` is also a cycle. In other words, cycles from a graph are preserved when they are mapped to a supergraph.
More concisely: If `G` is a subgraph of `G'`, and `p` is a closed walk forming a cycle in `G`, then the image of `p` under `SimpleGraph.Walk.mapLe` is also a cycle in `G'`.
|
SimpleGraph.Walk.reverse_cons
theorem SimpleGraph.Walk.reverse_cons :
∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
(SimpleGraph.Walk.cons h p).reverse = p.reverse.append (SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil)
This theorem, `SimpleGraph.Walk.reverse_cons`, states that for any simple graph `G` with vertices of type `V` and any three vertices `u`, `v`, and `w` in that graph such that `u` is adjacent to `v`, and there's a walk `p` from `v` to `w`, the reverse of the walk that starts at `u`, goes to `v` and then follows the walk `p` to `w`, is equal to the walk which first does the reverse of `p` and then goes from `v` to `u`. In other words, reversing a walk that begins with an edge preserves the structure of the walk, but with the direction of each edge and the order of the edges reversed.
More concisely: For any simple graph `G` and vertices `u`, `v`, `w` in `G` such that `u` is adjacent to `v` and there exists a walk `p` from `v` to `w`, the reverse walk from `u` to `v` followed by `p` is equal to the reverse of `p` followed by the walk from `v` to `u`.
|
SimpleGraph.Walk.IsCycle.of_mapLe
theorem SimpleGraph.Walk.IsCycle.of_mapLe :
∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
(SimpleGraph.Walk.mapLe h p).IsCycle → p.IsCycle
The theorem `SimpleGraph.Walk.IsCycle.of_mapLe` states that for any types `V`, given two simple graphs `G` and `G'` of type `V`, and a proof `h` that `G` is a subgraph of `G'`, for any vertex `u` of type `V`, and any walk `p` in `G` starting and ending at `u`, if the walk `p` mapped to the supergraph `G'` using `SimpleGraph.Walk.mapLe` with the proof `h` forms a cycle, then the original walk `p` in `G` also forms a cycle. In other words, if a walk forms a cycle in a supergraph, the corresponding walk in the subgraph also forms a cycle.
More concisely: If `h` is a proof that simple graph `G` is a subgraph of simple graph `G'`, and there exists a cycle in the image of any walk `p` in `G` starting and ending at some vertex `u` under the map `SimpleGraph.Walk.mapLe` from `G` to `G'` using `h`, then `p` itself forms a cycle in `G`.
|
SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts
theorem SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {d : G.Dart}, d ∈ p.darts → d.toProd.1 ∈ p.support
The theorem `SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts` states that for any type `V`, any simple graph `G` with vertices of type `V`, any vertices `u` and `v` of type `V`, any walk `p` from `u` to `v` in the graph `G`, and any dart `d` from the graph `G`, if dart `d` is in the list of darts that the walk `p` visits in order, then the first element of the pair that the dart `d` maps to (`d.toProd.1`) is in the list of vertices that the walk `p` visits in order. In other words, if a dart is used in a walk, then its originating vertex is visited in that walk.
More concisely: For any simple graph `G`, vertices `u` and `v`, walk `p` from `u` to `v`, and dart `d` in `G` on edge `(u, v)` in `p`, we have `u = fst (d.toProd)`.
|
SimpleGraph.Walk.map_isPath_iff_of_injective
theorem SimpleGraph.Walk.map_isPath_iff_of_injective :
∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G.Hom G'} {u v : V} {p : G.Walk u v},
Function.Injective ⇑f → ((SimpleGraph.Walk.map f p).IsPath ↔ p.IsPath)
The theorem `SimpleGraph.Walk.map_isPath_iff_of_injective` states that for any types `V` and `V'`, any simple graphs `G` and `G'` on `V` and `V'` respectively, any graph homomorphism `f` from `G` to `G'`, and any vertices `u` and `v` in `V`, if a walk `p` exists from `u` to `v` in `G`, and if the function `f` is injective, then the walk `p` is a path in `G` if and only if the walk `SimpleGraph.Walk.map f p` is a path in `G'`. In other words, an injective graph homomorphism preserves the property of being a path in the graph, when applied to any walk in the original graph.
More concisely: For any simple graphs G and G', injective graph homomorphisms f from G to G', and vertices u and v in the respective vertex sets, a walk from u to v in G is a path if and only if the image walk under f is a path in G'.
|
Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.36
theorem Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.36 :
∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.IsPath = True
This theorem, from the `Mathlib.Combinatorics.SimpleGraph.Connectivity` namespace in Lean 4, states that for any type `V`, any simple graph `G` of type `V`, and any vertex `u` of type `V`, a walk `p` in graph `G` starting and ending at vertex `u` is a path if and only if `p` is equivalent to the empty walk, `SimpleGraph.Walk.nil`. In other words, the only walk in a simple graph that can be considered a path and starts and ends at the same vertex is the one that does not contain any edges, the empty walk.
More concisely: In a simple graph, a walk starting and ending at the same vertex is a path if and only if it is the empty walk.
|
SimpleGraph.Walk.length_append
theorem SimpleGraph.Walk.length_append :
∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w),
(p.append q).length = p.length + q.length
This theorem states that for any simple graph `G` with vertices of type `V` and any three vertices `u`, `v`, and `w` in the graph, if there exists a walk `p` from `u` to `v` and a walk `q` from `v` to `w`, then the length of the walk obtained by appending `q` to `p` (in other words, the walk from `u` to `w` that first follows `p` and then follows `q`) is equal to the sum of the lengths of `p` and `q`. The length of a walk is defined as the number of edges or darts along it.
More concisely: For any simple graph, the length of a walk from one vertex to another through a third vertex is equal to the sum of the lengths of the walks between each pair of vertices.
|
SimpleGraph.Walk.support_append
theorem SimpleGraph.Walk.support_append :
∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
(p.append p').support = p.support ++ p'.support.tail
This theorem states that for any simple graph `G` with vertex type `V`, and any three vertices `u`, `v`, and `w`, if `p` is a walk from `u` to `v` and `p'` is a walk from `v` to `w`, then the list of vertices visited in order (the 'support') of the walk that appends `p'` to `p` is the concatenation of the 'support' of `p` and the 'support' of `p'`, excluding the first vertex of the 'support' of `p'` (since the vertex `v` is already included at the end of the 'support' of `p`).
More concisely: For any simple graph and vertices u, v, w, if there exist walks p from u to v and p' from v to w, then the support of the walk obtained by appending p' to p is the concatenation of the supports of p and p', with the first vertex of p's support excluded.
|
SimpleGraph.Walk.IsPath.of_mapLe
theorem SimpleGraph.Walk.IsPath.of_mapLe :
∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
(SimpleGraph.Walk.mapLe h p).IsPath → p.IsPath
The theorem `SimpleGraph.Walk.IsPath.of_mapLe` states that for any types `V` and simple graphs `G` and `G'` over `V`, if `G` is a subgraph of `G'` denoted by `G ≤ G'`, and `p` is a walk from vertex `u` to vertex `v` in `G`, then if the walk `p` mapped to the supergraph `G'` is a path, it follows that `p` is also a path in `G`. Here, a path is defined as a walk in the graph where no vertices are repeated.
More concisely: If `G` is a subgraph of `G'`, and `p` is a walk from vertex `u` to vertex `v` in `G` that maps to a path in `G'`, then `p` is a path in `G`.
|
SimpleGraph.Reachable.trans
theorem SimpleGraph.Reachable.trans :
∀ {V : Type u} {G : SimpleGraph V} {u v w : V}, G.Reachable u v → G.Reachable v w → G.Reachable u w
This theorem states that for any given SimpleGraph `G` with vertices of type `V`, and any three vertices `u`, `v`, and `w` in `G`, if `u` is reachable from `v`, and `v` is reachable from `w`, then `u` is also reachable from `w`. This property is known as transitivity in graph theory, which states that reachability in a graph is a transitive relation.
More concisely: In a simple graph, if there exist paths from vertex `v` to `u` and from vertex `u` to `w`, then there exists a path from vertex `v` to `w`.
|
Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.33
theorem Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.33 :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.IsTrail = p.IsTrail
The theorem `Mathlib.Combinatorics.SimpleGraph.Connectivity._auxLemma.33` states that for any type `V`, any simple graph `G` of vertices of type `V`, and any two vertices `u` and `v` of type `V`, a walk `p` from `u` to `v` in `G` is a path if and only if the list of vertices visited by the walk `p` (i.e., the `support` of `p`) has no duplicates. In other words, a walk in the graph is a path if it doesn't visit the same vertex twice.
More concisely: A walk in a simple graph between two vertices is a path if and only if it visits each vertex at most once.
|
SimpleGraph.ConnectedComponent.ind
theorem SimpleGraph.ConnectedComponent.ind :
∀ {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → Prop},
(∀ (v : V), β (G.connectedComponentMk v)) → ∀ (c : G.ConnectedComponent), β c
The theorem `SimpleGraph.ConnectedComponent.ind` states that for any type `V`, any simple graph `G` of this type, and any property `β` that applies to the connected components of `G`, if every vertex `v` in the graph `G` satisfies the property `β` when we consider its connected component (obtained via `SimpleGraph.connectedComponentMk G v`), then this property `β` holds for every connected component `c` of the graph `G`. In other words, this theorem is a form of induction principle for connected components of a graph, stating that if a property holds for every connected component containing a single vertex, then it holds for all connected components.
More concisely: If every vertex in a simple graph's connected component has property β, then every connected component of the graph has property β.
|
SimpleGraph.Walk.IsPath.mapLe
theorem SimpleGraph.Walk.IsPath.mapLe :
∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
p.IsPath → (SimpleGraph.Walk.mapLe h p).IsPath
This theorem, called `SimpleGraph.Walk.IsPath.mapLe`, states that for any two simple graphs `G` and `G'` of vertices `V` where `G` is a subgraph of `G'`, and for any two vertices `u` and `v` in `V`, if there exists a path `p` from `u` to `v` in `G` where `p` is a path (i.e., `p` contains no repeated edges), then the mapped path from `u` to `v` in `G'` is also a path. In other words, this theorem states that paths in a subgraph maintain their path property when mapped to the supergraph.
More concisely: If `G` is a subgraph of `G'`, and `p` is a path in `G` between vertices `u` and `v`, then the image of `p` under the graph homomorphism from `G` to `G'` is also a path between `u` and `v`.
|
SimpleGraph.Walk.darts_append
theorem SimpleGraph.Walk.darts_append :
∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (p' : G.Walk v w),
(p.append p').darts = p.darts ++ p'.darts
The theorem `SimpleGraph.Walk.darts_append` states that for any simple graph `G` with vertices of some type `V`, and any three vertices `u`, `v`, and `w` in the graph, if `p` is a walk from `u` to `v` and `p'` is a walk from `v` to `w`, then the list of darts (edges directed from one vertex to another) visited in the walk from `u` to `w` (which is the concatenation of `p` and `p'`) is the same as the concatenation of the list of darts visited in `p` and the list of darts visited in `p'`. In other words, the ordering of the darts visited in the combined walk is the same as the ordering of the darts in the individual walks.
More concisely: Given a simple graph with vertices of type `V` and walks `p` from vertex `u` to vertex `v` and `p'` from vertex `v` to vertex `w`, the list of darts visited in the walk from `u` to `w` (the concatenation of `p` and `p'`) is equal to the concatenation of the lists of darts visited in `p` and `p'`.
|
SimpleGraph.Walk.isTrail_def
theorem SimpleGraph.Walk.isTrail_def :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.IsTrail ↔ p.edges.Nodup
This theorem states that for any simple graph `G` with vertices of type `V`, and any walk `p` from vertex `u` to vertex `v` in `G`, the walk `p` is a trail if and only if the list of edges visited by `p` has no duplicates. In other words, a walk is defined as a trail when each edge in the graph is visited at most once.
More concisely: A simple graph walk from vertex `u` to vertex `v` is a trail if and only if the set of edges visited during the walk is a subset of the graph's edge set with no repeated elements.
|
SimpleGraph.Walk.mem_support_nil_iff
theorem SimpleGraph.Walk.mem_support_nil_iff :
∀ {V : Type u} {G : SimpleGraph V} {u v : V}, u ∈ SimpleGraph.Walk.nil.support ↔ u = v
This theorem states that for any given simple graph `G` with vertices of type `V`, and any two vertices `u` and `v`, the vertex `u` is in the support of the nil walk (the walk that visits no edges) from `u` to `v` if and only if `u` is equal to `v`. In other words, the only vertex visited in a nil walk is the endpoint `v`, so for `u` to be in the support of such a walk, it must be the same as `v`.
More concisely: In a simple graph, a vertex is in the support of the nil walk (visit no edges) between two vertices if and only if the vertices are equal.
|
SimpleGraph.ConnectedComponent.eq
theorem SimpleGraph.ConnectedComponent.eq :
∀ {V : Type u} {G : SimpleGraph V} {v w : V},
G.connectedComponentMk v = G.connectedComponentMk w ↔ G.Reachable v w
The theorem `SimpleGraph.ConnectedComponent.eq` states that for any given simple graph `G` of vertices of type `V`, and any two vertices `v` and `w` of that graph, the connected component containing vertex `v` is the same as the connected component containing vertex `w` if and only if `v` and `w` are reachable from each other. In other words, there exists a walk in the graph `G` from vertex `v` to vertex `w`.
More concisely: Two vertices `v` and `w` of a simple graph `G` belong to the same connected component if and only if they are reachable from each other.
|
SimpleGraph.coe_finsetWalkLength_eq
theorem SimpleGraph.coe_finsetWalkLength_eq :
∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (n : ℕ) (u v : V),
↑(G.finsetWalkLength n u v) = {p | p.length = n}
The theorem `SimpleGraph.coe_finsetWalkLength_eq` states that for any simple graph `G` of vertices of type `V` (where `V` has decidable equality and `G` is locally finite), and for any two vertices `u` and `v` in `G` and a natural number `n`, the set of all walks from `u` to `v` of length `n` (as a subset of the type of all walks) is equal to the set of all walks `p` such that the length of `p` is `n`. This means that the function `SimpleGraph.finsetWalkLength` correctly computes the set of walks of a given length between two vertices in a simple, locally finite graph.
More concisely: For any simple graph of decidably equalvertices and finite degree, the set of walks of length n between two vertices equals the set of walks of length n from the first vertex to the second vertex.
|
SimpleGraph.Walk.isPath_def
theorem SimpleGraph.Walk.isPath_def :
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.IsPath ↔ p.support.Nodup
The theorem `SimpleGraph.Walk.isPath_def` states that for any given simple graph `G` with vertices of type `V`, and for any walk `p` in the graph `G` from vertex `u` to vertex `v`, the walk `p` is a path if and only if the list of vertices visited in order (`SimpleGraph.Walk.support p`) has no duplicates (`List.Nodup`). In other words, a walk `p` is a path in a simple graph `G` precisely when it visits each vertex at most once.
More concisely: A simple graph walk is a path if and only if the vertices visited in the order of the walk have no repetitions.
|