adj_iff_of_neighborSet_equiv — Mathlib

English

If G.neighborSet v ≃ H.neighborSet v with finiteness, then H.Adj v w ↔ G.Adj v w for all w.

Русский

Если G.neighborSet v эквивалентно H.neighborSet v и оба конечны, то для любого w выполняется H.Adj v w ⇔ G.Adj v w.

LaTeX

$$$\forall {w},\ H.Adj v w \iff G.Adj v w$$$

Lean4

theorem adj_iff_of_neighborSet_equiv {v : V} {H : Subgraph G} (h : G.neighborSet v ≃ H.neighborSet v)
    (hfin : (G.neighborSet v).Finite) : ∀ {w}, H.Adj v w ↔ G.Adj v w :=
  Set.ext_iff.mp (neighborSet_eq_of_equiv h hfin) _

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