mapNeighborSet — Mathlib

English

A copy induces an embedding from the neighbor set of a vertex to the neighbor set of its image.

Русский

Копия индуцирует вложение множеств соседей вершины в множество соседей образа вершины.

LaTeX

$$(f : Copy A B) (a : α) : A.neighborSet a ↪ B.neighborSet (f a)$$

Lean4

/-- A copy induces an embedding of neighbor sets. -/
def mapNeighborSet (f : Copy A B) (a : α) : A.neighborSet a ↪ B.neighborSet (f a)
    where
  toFun v := ⟨f v, f.toHom.apply_mem_neighborSet v.prop⟩
  inj' _ _
    h := by
    rw [Subtype.mk_eq_mk] at h ⊢
    exact f.injective h

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