reachable_iff — Mathlib

English

If φ: G ≃g G' is an isomorphism, then G'.Reachable(φ u)(φ v) ↔ G.Reachable u v.

Русский

Если φ — изоморфизм графов G и G', тогда достижимость сохраняется под изоморфизмом: G'.Reachable(φ u)(φ v) ⇔ G.Reachable u v.

LaTeX

$$$\,\text{theorem }(G,G',\phi): G'.Reachable (\phi u) (\phi v) \iff G.Reachable u v.$$$

Lean4

theorem reachable_iff {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u v : V} :
    G'.Reachable (φ u) (φ v) ↔ G.Reachable u v :=
  ⟨fun r => φ.left_inv u ▸ φ.left_inv v ▸ r.map φ.symm.toHom, Reachable.map φ.toHom⟩

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