Commit 2023-05-08 02:51 296aaf3b

View on Github →

feat: port Topology.Category.Top.OpenNhds (#3834)

Estimated changes

Modified Mathlib.lean

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

added def IsOpenMap.adjunctionNhds

added def IsOpenMap.functorNhds

added def TopologicalSpace.OpenNhds.inclusion

added def TopologicalSpace.OpenNhds.inclusionMapIso

added theorem TopologicalSpace.OpenNhds.inclusionMapIso_hom

added theorem TopologicalSpace.OpenNhds.inclusionMapIso_inv

added theorem TopologicalSpace.OpenNhds.inclusion_obj

added def TopologicalSpace.OpenNhds.infLeLeft

added def TopologicalSpace.OpenNhds.infLeRight

added def TopologicalSpace.OpenNhds.map

added theorem TopologicalSpace.OpenNhds.map_id_obj'

added theorem TopologicalSpace.OpenNhds.map_id_obj

added theorem TopologicalSpace.OpenNhds.map_id_obj_unop

added theorem TopologicalSpace.OpenNhds.map_obj

added theorem TopologicalSpace.OpenNhds.op_map_id_obj

added theorem TopologicalSpace.OpenNhds.openEmbedding

added def TopologicalSpace.OpenNhds