Commit 2023-08-01 18:11 067dad6d

View on Github →

feat(Topology/Order/UpperLowerSetTopology): Introduce the Upper Set (or Alexandrov) topology and the Lower Set topology (#5672) Introduces the Upper Set topology, which is the canonical example of an Alexandrov topology and its dual, the Lower Set topology.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Order/UpperLowerSetTopology.lean

added theorem LowerSetDual_iff_UpperSet

added theorem LowerSetTopology.IsOpen_iff_IsLowerSet

added theorem LowerSetTopology.IsOpen_sInter

added theorem LowerSetTopology.LowerSetLELower

added theorem LowerSetTopology.Monotone_to_LowerTopology_Continuous

added theorem LowerSetTopology.closure_eq_upperClosure

added theorem LowerSetTopology.closure_singleton

added theorem LowerSetTopology.isClosed_iff_isUpper

added theorem LowerSetTopology.isClosed_isUpper

added theorem LowerSetTopology.isOpen_iInter

added theorem LowerSetTopology.topology_eq

added def LowerSetTopology.withLowerSetTopologyHomeomorph

added def UpperLowerSet_toOrderDualHomeomorph

added theorem UpperSetDual_iff_LowerSet

added theorem UpperSetTopology.IsOpen_iff_IsUpperSet

added theorem UpperSetTopology.IsOpen_sInter

added theorem UpperSetTopology.Monotone_to_UpperTopology_Continuous

added theorem UpperSetTopology.UpperSetLEUpper

added theorem UpperSetTopology.closure_eq_lowerClosure

added theorem UpperSetTopology.closure_singleton

added theorem UpperSetTopology.isClosed_iff_isLower

added theorem UpperSetTopology.isClosed_isLower

added theorem UpperSetTopology.isOpen_iInter

added theorem UpperSetTopology.topology_eq

added def UpperSetTopology.withUpperSetTopologyHomeomorph

added def WithLowerSetTopology.ofLowerSet

added def WithLowerSetTopology.ofLowerSetOrderIso

added theorem WithLowerSetTopology.ofLowerSet_inj

added theorem WithLowerSetTopology.ofLowerSet_le_iff

added theorem WithLowerSetTopology.ofLowerSet_toLowerSet

added theorem WithLowerSetTopology.of_withLowerSetTopology_symm_eq

added def WithLowerSetTopology.toLowerSet

added def WithLowerSetTopology.toLowerSetOrderIso

added theorem WithLowerSetTopology.toLowerSet_inj

added theorem WithLowerSetTopology.toLowerSet_le_iff

added theorem WithLowerSetTopology.toLowerSet_ofLowerSet

added theorem WithLowerSetTopology.to_withLowerSetTopology_symm_eq

added def WithLowerSetTopology

added def WithUpperSetTopology.ofUpperSet

added def WithUpperSetTopology.ofUpperSetOrderIso

added theorem WithUpperSetTopology.ofUpperSet_inj

added theorem WithUpperSetTopology.ofUpperSet_le_iff

added theorem WithUpperSetTopology.ofUpperSet_toUpperSet

added theorem WithUpperSetTopology.of_withUpperSetTopology_symm_eq

added def WithUpperSetTopology.toUpperSet

added def WithUpperSetTopology.toUpperSetOrderIso

added theorem WithUpperSetTopology.toUpperSet_inj

added theorem WithUpperSetTopology.toUpperSet_le_iff

added theorem WithUpperSetTopology.toUpperSet_ofUpperSet

added theorem WithUpperSetTopology.to_withUpperSetTopology_symm_eq

added def WithUpperSetTopology

added def lowerSetTopology'

added def upperSetTopology'