mapNeighborSet — Mathlib

English

A graph isomorphism f provides a bijection between the neighbor set of a vertex v in G and the neighbor set of f(v) in G'.

Русский

Граф-изоморфизм f задаёт биекцию между множеством соседей вершины v в G и множеством соседей вершины f(v) в G'.

LaTeX

$$$ \forall v \in V,\ G.neighborSet(v) \cong G'.neighborSet(f(v)) $$$

Lean4

/-- A graph isomorphism induces an equivalence of neighbor sets. -/
@[simps]
def mapNeighborSet (v : V) : G.neighborSet v ≃ G'.neighborSet (f v)
    where
  toFun w := ⟨f w, f.apply_mem_neighborSet_iff.mpr w.2⟩
  invFun w := ⟨f.symm w, by simpa [RelIso.symm_apply_apply] using f.symm.apply_mem_neighborSet_iff.mpr w.2⟩
  left_inv w := by simp
  right_inv w := by simp

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