pathGraph3ComplEmbedding — Mathlib

English

Any IsPathGraph3Compl in G gives rise to an embedding of the complement of the path graph on 3 into G.

Русский

Любое IsPathGraph3Compl в G порождает вложение комплемента графа пути на 3 вершины в G.

LaTeX

$$pathGraph3ComplEmbedding$$

Lean4

/-- Any `IsPathGraph3Compl` in `G` gives rise to a graph embedding of the complement of the path graph
-/
def pathGraph3ComplEmbedding {v w₁ w₂ : α} (h : G.IsPathGraph3Compl v w₁ w₂) : (pathGraph 3)ᶜ ↪g G
    where
  toFun := fun x ↦
    match x with
    | 0 => w₁
    | 1 => v
    | 2 => w₂
  inj' := by
    intro _ _ _
    have := h.ne_fst
    have := h.ne_snd
    have := h.adj.ne
    aesop
  map_rel_iff' := by
    intro _ _
    simp_rw [Function.Embedding.coeFn_mk, compl_adj, ne_eq, pathGraph_adj, not_or]
    have := h.adj
    have := h.adj.symm
    have h1 := h.not_adj_fst
    have h2 := h.not_adj_snd
    have ⟨_, _⟩ : ¬G.Adj w₁ v ∧ ¬G.Adj w₂ v := by rw [adj_comm] at h1 h2; exact ⟨h1, h2⟩
    aesop

Похожие утверждения