SimpleGraph.adj_replaceVertex_iff_of_ne_left
theorem SimpleGraph.adj_replaceVertex_iff_of_ne_left :
∀ {V : Type u_1} [inst : DecidableEq V] (G : SimpleGraph V) (s : V) {t w : V},
w ≠ t → ((G.replaceVertex s t).Adj s w ↔ G.Adj s w)
This theorem, named `SimpleGraph.adj_replaceVertex_iff_of_ne_left`, states that for any type `V` that has decidable equality, given a simple graph `G` defined over `V`, a vertex `s` in `V`, and vertices `t` and `w` in `V` such that `w` is not equal to `t`, the adjacency of `s` and `w` in the graph obtained by replacing `s` with `t` in `G` is equivalent to the adjacency of `s` and `w` in `G`, except possibly when `t` is considered. In other words, except for the vertex `t`, the neighbors of `s` in the graph formed by replacing `s` with `t` in `G` are the same as its neighbors in `G`.
More concisely: Given a simple graph and replacing a vertex with another non-equal vertex preserves adjacency for all other vertices.
|
SimpleGraph.adj_replaceVertex_iff_of_ne_right
theorem SimpleGraph.adj_replaceVertex_iff_of_ne_right :
∀ {V : Type u_1} [inst : DecidableEq V] (G : SimpleGraph V) (s : V) {t w : V},
w ≠ t → ((G.replaceVertex s t).Adj t w ↔ G.Adj s w)
This theorem states that in a Simple Graph `G` with vertices of an arbitrary type `V` (where equality of vertices `V` is decidable), for any vertices `s`, `t`, and `w` (where `w` is not equal to `t`), the adjacency of `t` and `w` in the graph obtained by replacing vertex `s` with `t` in `G` is equivalent to the adjacency of `s` and `w` in `G`, except possibly when `t` equals itself. In other words, except for `t` itself, the neighbors of `t` in the graph obtained by replacing `s` with `t` are the same as the neighbors of `s` in the original graph `G`.
More concisely: In a simple graph with decidable vertex equality, replacing vertex `s` with `t` preserves adjacency between `s` and `w` (except for the case where `t` equals `w`).
|
Mathlib.Combinatorics.SimpleGraph.Operations._auxLemma.1
theorem Mathlib.Combinatorics.SimpleGraph.Operations._auxLemma.1 :
∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] {a : α}, (a ∈ s.toFinset) = (a ∈ s)
This theorem asserts that for any type `α`, any set `s` of type `α`, and any element `a` of type `α`, `a` is a member of the finset equivalent of `s` if and only if `a` is a member of the set `s`. In other words, conversion of a set `s` to its finset form via `Set.toFinset` preserves the membership of elements.
More concisely: For any type `α`, any set `s` of type `α`, and any element `a` of type `α`, `a` is in the finset `Set.toFinset s` if and only if `a` is in the set `s`.
|
SimpleGraph.not_adj_replaceVertex_same
theorem SimpleGraph.not_adj_replaceVertex_same :
∀ {V : Type u_1} [inst : DecidableEq V] (G : SimpleGraph V) (s t : V), ¬(G.replaceVertex s t).Adj s t
This theorem states that for any type `V` with decidable equality, any simple graph `G` of vertices of type `V`, and any two vertices `s` and `t` of type `V`, there is never an edge between `s` and `t` in the graph obtained by replacing vertex `s` with vertex `t` in `G`. In other words, after the replacement operation, `s` and `t` are not adjacent in the new graph.
More concisely: For any decidably equal type `V` and simple graph `G` over `V`, if we replace a vertex `s` with another vertex `t`, there are no edges between `s` and `t` in the resulting graph.
|
SimpleGraph.adj_replaceVertex_iff_of_ne
theorem SimpleGraph.adj_replaceVertex_iff_of_ne :
∀ {V : Type u_1} [inst : DecidableEq V] (G : SimpleGraph V) (s : V) {t v w : V},
v ≠ t → w ≠ t → ((G.replaceVertex s t).Adj v w ↔ G.Adj v w)
The theorem `SimpleGraph.adj_replaceVertex_iff_of_ne` states that for any vertices `v` and `w` in a Simple Graph `G` of type `V` with decidable equality, if `v` and `w` are not equal to a vertex `t`, then the adjacency of `v` and `w` in the graph obtained by replacing vertex `s` with vertex `t` in `G` (denoted as `G.replaceVertex s t`) is the same as their adjacency in the original graph `G`. In other words, if we replace a vertex `s` with a vertex `t` in a graph, the adjacency between all other vertices remains unchanged.
More concisely: For any simple graph G of type V with decidable equality, vertices v and w are adjacent in G.replaceVertex s t if and only if they are adjacent in G, provided v, w, and s are distinct.
|