Mathlib.Combinatorics.SimpleGraph.Maps._auxLemma.2
theorem Mathlib.Combinatorics.SimpleGraph.Maps._auxLemma.2 :
∀ {V : Type u_1} {W : Type u_2} {u v : V} {G : SimpleGraph W} {f : V → W},
(SimpleGraph.comap f G).Adj u v = G.Adj (f u) (f v)
This theorem states that for any types `V` and `W`, any vertices `u` and `v` of type `V`, any simple graph `G` of type `W`, and any function `f` from `V` to `W`, the adjacency in the graph induced by the function `f` from `G` on the vertices `u` and `v` is the same as the adjacency in the original graph `G` between the images of `u` and `v` under the function `f`. In other words, a function `f` induces a simple graph on `V` from a simple graph on `W` by preserving the adjacency relation.
More concisely: For any simple graphs G on type W, functions f from type V to W, and vertices u, v of type V, the adjacency relation between u and v in the graph induced by f from G holds if and only if the images of u and v under f are adjacent in G.
|
SimpleGraph.Iso.apply_mem_neighborSet_iff
theorem SimpleGraph.Iso.apply_mem_neighborSet_iff :
∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G.Iso G') {v w : V},
f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v
The theorem `SimpleGraph.Iso.apply_mem_neighborSet_iff` states that for any types `V` and `W` and for any simple graphs `G` of type `V` and `G'` of type `W`, if there is a graph isomorphism `f` between `G` and `G'`, then for any vertices `v` and `w` of `G`, `w` is in the neighbor set of `v` in `G` if and only if the image of `w` under `f` is in the neighbor set of the image of `v` under `f` in `G'`. In other words, the graph isomorphism `f` preserves the adjacency relationship between vertices.
More concisely: For simple graphs G of type V and G' of type W, if there is a graph isomorphism f between them, then v and w are adjacent in G if and only if the images of v and w under f are adjacent in G'.
|
SimpleGraph.Hom.injective_of_top_hom
theorem SimpleGraph.Hom.injective_of_top_hom :
∀ {V : Type u_1} {W : Type u_2} {G' : SimpleGraph W} (f : ⊤.Hom G'), Function.Injective ⇑f
The theorem `SimpleGraph.Hom.injective_of_top_hom` states that every graph homomorphism from a complete graph to any other graph is injective. In other words, for all vertices `V` and `W`, and for any simple graph `G'` on `W`, if we have a function `f` which is a homomorphism from the complete graph on `V` to `G'`, then this function `f` has the property that if it maps two vertices to the same vertex, then those two vertices were the same to begin with. This is the mathematical concept of injectivity applied to graph homomorphisms.
More concisely: Every homomorphism from a complete graph to a simple graph is injective.
|
SimpleGraph.Embedding.map_adj_iff
theorem SimpleGraph.Embedding.map_adj_iff :
∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G.Embedding G') {v w : V},
G'.Adj (f v) (f w) ↔ G.Adj v w
This theorem states that for any types `V` and `W`, and any simple graphs `G` of type `V` and `G'` of type `W`, and for any embedding `f` from `G` to `G'`, and any vertices `v` and `w` in `G`, the vertices `f(v)` and `f(w)` in `G'` are adjacent if and only if `v` and `w` in `G` are adjacent. In other words, the embedding `f` preserves adjacency relationships between vertices.
More concisely: For any simple graph embeddings f between types V and W, if v and w are adjacent vertices in the graph V, then f(v) and f(w) are adjacent vertices in the graph W.
|
Mathlib.Combinatorics.SimpleGraph.Maps._auxLemma.1
theorem Mathlib.Combinatorics.SimpleGraph.Maps._auxLemma.1 :
∀ {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph V) (u v : W),
(SimpleGraph.map f G).Adj u v = ∃ u' v', G.Adj u' v' ∧ f u' = u ∧ f v' = v
This theorem states that for any two types `V` and `W`, given an injective function `f` from `V` to `W` and a simple graph `G` on `V`, for any two elements `u` and `v` from `W`, the adjacency in the graph obtained by applying the function `f` to `G` (`SimpleGraph.map f G`) between `u` and `v` is equivalent to the existence of two elements `u'` and `v'` in `V` such that `u'` and `v'` are adjacent in the original graph `G` and the images of `u'` and `v'` under the function `f` are `u` and `v` respectively. In other words, the mapped graph preserves the adjacency structure of the original graph under the injective function `f`.
More concisely: For any injective function between types `V` and `W` and simple graph `G` on `V`, elements `u` and `v` in `W` are adjacent in the mapped graph `SimpleGraph.map f G` if and only if there exist adjacent elements `u'` and `v'` in `G` such that `f(u') = u` and `f(v') = v`.
|
SimpleGraph.Hom.map_adj
theorem SimpleGraph.Hom.map_adj :
∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G.Hom G') {v w : V},
G.Adj v w → G'.Adj (f v) (f w)
This theorem, `SimpleGraph.Hom.map_adj`, states that for any two types `V` and `W`, and any two simple graphs `G` of type `V` and `G'` of type `W`, if there is a graph homomorphism `f` from `G` to `G'`, then for any two vertices `v` and `w` in `G`, if `v` and `w` are adjacent in `G` (i.e., there is an edge between them), then the images of `v` and `w` under `f` (i.e., `f v` and `f w`) are also adjacent in `G'`. In short, the adjacency relationship between two vertices is preserved under a graph homomorphism.
More concisely: Given simple graphs G of type V and G' of type W, and a graph homomorphism f from G to G', if v and w are adjacent vertices in G, then f(v) and f(w) are adjacent vertices in G'.
|