Commit 2023-02-11 09:23 4be13d06

View on Github →

feat: port Topology.Order.LowerTopology (#2163)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Order/LowerTopology.lean

added theorem LowerTopology.closure_singleton

added theorem LowerTopology.continuous_of_Ici

added theorem LowerTopology.isClosed_Ici

added theorem LowerTopology.isClosed_upperClosure

added theorem LowerTopology.isLowerSet_of_isOpen

added theorem LowerTopology.isOpen_iff_generate_Ici_compl

added theorem LowerTopology.isUpperSet_of_isClosed

added def LowerTopology.lowerBasis

added theorem LowerTopology.topology_eq

added def LowerTopology.withLowerTopologyHomeomorph

added theorem WithLowerTopology.isOpen_def

added theorem WithLowerTopology.isOpen_preimage_ofLower

added def WithLowerTopology.ofLower

added theorem WithLowerTopology.ofLower_inj

added theorem WithLowerTopology.ofLower_toLower

added theorem WithLowerTopology.of_withLowerTopology_symm_eq

added def WithLowerTopology.toLower

added theorem WithLowerTopology.toLower_inj

added theorem WithLowerTopology.toLower_ofLower

added theorem WithLowerTopology.to_withLowerTopology_symm_eq

added def WithLowerTopology