Commit 2023-04-27 02:37 48a2b71a

View on Github →

feat: port Topology.Category.Top.Opens (#3662)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/Top/Opens.lean

added def IsOpenMap.adjunction

added def IsOpenMap.functor

added theorem TopologicalSpace.Opens.adjunction_counit_app_self

added theorem TopologicalSpace.Opens.adjunction_counit_map_functor

added theorem TopologicalSpace.Opens.functor_map_eq_inf

added theorem TopologicalSpace.Opens.functor_obj_map_obj

added def TopologicalSpace.Opens.inclusion

added def TopologicalSpace.Opens.inclusionTopIso

added theorem TopologicalSpace.Opens.inclusion_map_eq_top

added theorem TopologicalSpace.Opens.inclusion_top_functor

added theorem TopologicalSpace.Opens.infLeLeft_apply

added theorem TopologicalSpace.Opens.infLeLeft_apply_mk

added theorem TopologicalSpace.Opens.leSupr_apply_mk

added def TopologicalSpace.Opens.map

added def TopologicalSpace.Opens.mapComp

added def TopologicalSpace.Opens.mapId

added def TopologicalSpace.Opens.mapIso

added theorem TopologicalSpace.Opens.mapIso_hom_app

added theorem TopologicalSpace.Opens.mapIso_inv_app

added theorem TopologicalSpace.Opens.mapIso_refl

added def TopologicalSpace.Opens.mapMapIso

added theorem TopologicalSpace.Opens.map_coe

added theorem TopologicalSpace.Opens.map_comp_eq

added theorem TopologicalSpace.Opens.map_comp_map

added theorem TopologicalSpace.Opens.map_comp_obj'

added theorem TopologicalSpace.Opens.map_comp_obj

added theorem TopologicalSpace.Opens.map_comp_obj_unop

added theorem TopologicalSpace.Opens.map_eq

added theorem TopologicalSpace.Opens.map_functor_eq'

added theorem TopologicalSpace.Opens.map_functor_eq

added theorem TopologicalSpace.Opens.map_id_eq

added theorem TopologicalSpace.Opens.map_id_obj'

added theorem TopologicalSpace.Opens.map_id_obj

added theorem TopologicalSpace.Opens.map_id_obj_unop

added theorem TopologicalSpace.Opens.map_obj

added theorem TopologicalSpace.Opens.map_supᵢ

added theorem TopologicalSpace.Opens.op_map_comp_obj

added theorem TopologicalSpace.Opens.op_map_id_obj

added theorem TopologicalSpace.Opens.openEmbedding

added theorem TopologicalSpace.Opens.openEmbedding_obj_top

added theorem TopologicalSpace.Opens.set_range_forget_map_inclusion

added def TopologicalSpace.Opens.toTopCat

added theorem TopologicalSpace.Opens.toTopCat_map