English
A homeomorphism induces an order-preserving equivalence on open sets via comaps.
Русский
Гомоморфизм по топологическим структурам индуцирует упорядоченное эквивалентное отображение на открытые множества через обратные изображения.
LaTeX
$$$\text{Homeomorph.opensCongr }(f) : Opens\,\alpha \simeq_{o} Opens\,\beta$$$
Lean4
/-- A homeomorphism induces an order-preserving equivalence on open sets, by taking comaps. -/
@[simps -fullyApplied apply]
def _root_.Homeomorph.opensCongr (f : α ≃ₜ β) : Opens α ≃o Opens β
where
toFun := Opens.comap (f.symm : C(β, α))
invFun := Opens.comap (f : C(α, β))
left_inv _ := ext <| f.toEquiv.preimage_symm_preimage _
right_inv _ := ext <| f.toEquiv.symm_preimage_preimage _
map_rel_iff' := by simp only [← SetLike.coe_subset_coe]; exact f.symm.surjective.preimage_subset_preimage_iff
