preconnected_iff — Mathlib

English

Connectivity (preconnected) is preserved under graph isomorphisms.

Русский

Связанность (предсвязность) сохраняется при изоморфизма графов.

LaTeX

$$$\forall G\,\forall H\,\forall e : G \simeq_g H,\ G.Preconnected \iff H.Preconnected$$$

Lean4

theorem preconnected_iff {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H) : G.Preconnected ↔ H.Preconnected :=
  ⟨Preconnected.map e.toHom e.toEquiv.surjective, Preconnected.map e.symm.toHom e.symm.toEquiv.surjective⟩

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