symm_apply_reachable — Mathlib

English

In terms of an isomorphism φ, reachable between φ.symm v and u in G is equivalent to reachable between v and φ u in G'.

Русский

При изоморфизме φ достижимо между φ.symm v и u в G эквивалентно достижимости между v и φ u в G'.

LaTeX

$$$G.Reachable (φ.symm v) u \iff G'.Reachable v (φ u).$$$

Lean4

theorem symm_apply_reachable {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u : V} {v : V'} :
    G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u) := by rw [← Iso.reachable_iff, RelIso.apply_symm_apply]

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