English
The isomorphism-induced equivalence between components induces an equivalence between their supports.
Русский
Эквиваленция компонент, порожденная изоморфизмом, индуцирует эквиваленцию между их опорами.
LaTeX
$$$\\text{isoEquivSupp}(\\\\phi : G \\\\simeq G') : C.supp \\\\cong (\\\\phi.connectedComponentEquiv C).supp$$$
Lean4
/-- The equivalence between connected components, induced by an isomorphism of graphs,
itself defines an equivalence on the supports of each connected component.
-/
def isoEquivSupp (φ : G ≃g G') (C : G.ConnectedComponent) : C.supp ≃ (φ.connectedComponentEquiv C).supp
where
toFun v := ⟨φ v, ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp.mpr v.prop⟩
invFun v' := ⟨φ.symm v', ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map.mpr v'.prop⟩
left_inv v := Subtype.ext (φ.toEquiv.left_inv ↑v)
right_inv v := Subtype.ext (φ.toEquiv.right_inv ↑v)
