mapNeighborSet — Mathlib

English

For a graph embedding f : G ↪g G' and a vertex v ∈ V, the map mapNeighborSet v : G.neighborSet(v) ↪ G'.neighborSet (f v) is an embedding.

Русский

Для вложения графа f: G ↪g G' и вершины v ∈ V отображение mapNeighborSet v : G.neighborSet(v) ↪ G'.neighborSet (f(v)) образует вложение.

LaTeX

$$$ G.neighborSet(v) \hookrightarrow G'.neighborSet (f(v)) $$$

Lean4

/-- A graph embedding induces an embedding 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⟩
  inj' := by
    rintro ⟨w₁, h₁⟩ ⟨w₂, h₂⟩ h
    rw [Subtype.mk_eq_mk] at h ⊢
    exact f.inj' h

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