pathGraph_two_embedding — Mathlib

English

There exists an embedding of pathGraph 2 into pathGraph n for n ≥ 2, mapping the two vertices of P2 to the first two vertices of Pn.

Русский

Существует вложение pathGraph(2) в pathGraph(n) для n ≥ 2, отображающее две вершины P2 в первые две вершины Pn.

LaTeX

$$pathGraph 2 ↪g pathGraph n$$

Lean4

/-- Embedding of `pathGraph 2` into the first two elements of `pathGraph n` for `2 ≤ n` -/
def pathGraph_two_embedding (n : ℕ) (h : 2 ≤ n) : pathGraph 2 ↪g pathGraph n
    where
  toFun v := ⟨v, trans v.2 h⟩
  inj' := by
    rintro v w
    rw [Fin.mk.injEq]
    exact Fin.ext
  map_rel_iff' := by
    intro v w
    fin_cases v <;> fin_cases w <;> simp [pathGraph, ← Fin.coe_covBy_iff]

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