Preimages of opens along an isomorphism of topological spaces

For an isomorphism f : X ≅ Y in TopCat, taking preimages along f.hom and along f.inv are the two directions of the order isomorphism Homeomorph.opensCongr of the homeomorphism TopCat.homeoOfIso f, so the two round trips are the identity on opens. Mathlib records this as the equivalence of categories TopologicalSpace.Opens.mapMapIso; this file records the two round trips as equalities of opens, the form met when an open of Y is compared with the preimage of its preimage.

Main results

• TopologicalSpace.Opens.map_hom_obj_map_inv_obj, TopologicalSpace.Opens.map_inv_obj_map_hom_obj: the preimage along f.hom of the preimage along f.inv of an open is that open, and the other way round.

@[simp]

theorem TopologicalSpace.Opens.map_hom_obj_map_inv_obj {X Y : TopCat} (f : X ≅ Y) (U : Opens ↑X) : (map f.hom).obj ((map f.inv).obj U) = U

The preimage along f.hom of the preimage along f.inv of an open U of X is U.

@[simp]

theorem TopologicalSpace.Opens.map_inv_obj_map_hom_obj {X Y : TopCat} (f : X ≅ Y) (U : Opens ↑Y) : (map f.inv).obj ((map f.hom).obj U) = U

The preimage along f.inv of the preimage along f.hom of an open U of Y is U.