coeNeighborSetEquiv — Mathlib

English

There is a natural equivalence between the neighbor set in the subgraph viewed via the coe and the neighbor set in the subgraph viewed in G.

Русский

Существует естественное эквивалентное отображение между множеством соседей в подграфе, рассматриваемым через встроение в подграф, и между множеством соседей в подграфе, рассматриваемым как подграф графа G.

LaTeX

$$$G'.\\text{coe.neighborSet}(v) \\simeq G'.\\text{neighborSet}(v)$$$

Lean4

/-- A subgraph as a graph has equivalent neighbor sets. -/
def coeNeighborSetEquiv {G' : Subgraph G} (v : G'.verts) : G'.coe.neighborSet v ≃ G'.neighborSet v
    where
  toFun w := ⟨w, w.2⟩
  invFun w := ⟨⟨w, G'.edge_vert (G'.adj_symm w.2)⟩, w.2⟩

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