Commit 2023-07-25 10:57 86c30b0e

View on Github →

feat(Topology/Order/LowerUpperTopology): Dual the lower topology (#5873) Defines the upper topology, which is the dual of the lower topology on a preorder.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Topology/Order/LowerTopology.lean to Mathlib/Topology/Order/LowerUpperTopology.lean

added theorem LowerDual_iff_Upper

added theorem UpperDual_iff_Lower

added theorem UpperTopology.closure_singleton

added theorem UpperTopology.continuous_of_Iic

added theorem UpperTopology.isClosed_Iic

added theorem UpperTopology.isClosed_lowerClosure

added theorem UpperTopology.isLowerSet_of_isClosed

added theorem UpperTopology.isOpen_iff_generate_Iic_compl

added theorem UpperTopology.isUpperSet_of_isOpen

added theorem UpperTopology.topology_eq

added def UpperTopology.upperBasis

added def UpperTopology.withUpperTopologyHomeomorph

added theorem WithUpperTopology.isOpen_def

added theorem WithUpperTopology.isOpen_preimage_ofUpper

added def WithUpperTopology.ofUpper

added theorem WithUpperTopology.ofUpper_inj

added theorem WithUpperTopology.ofUpper_toUpper

added theorem WithUpperTopology.of_withUpperTopology_symm_eq

added def WithUpperTopology.toUpper

added theorem WithUpperTopology.toUpper_inj

added theorem WithUpperTopology.toUpper_ofUpper

added theorem WithUpperTopology.to_withUpperTopology_symm_eq

added def WithUpperTopology

added def toOrderDualHomeomorph