Commit 2023-09-18 13:50 5553d1d4

View on Github →

fix(Topology/Order/UpperLowerSetTopology): Fix theorem names in UpperLowerSetTopology to match mathlib4 conventions (#6557) Modify lemma names in UpperLowerSetTopology to meet Mathlib4 conventions.

Estimated changes

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

added def WithLowerTopology.toDualHomeomorph

deleted def toOrderDualHomeomorph

Modified Mathlib/Topology/Order/UpperLowerSetTopology.lean

deleted theorem LowerSetDual_iff_UpperSet

deleted theorem LowerSetTopology.IsOpen_iff_IsLowerSet

deleted theorem LowerSetTopology.LowerSetLELower

deleted theorem LowerSetTopology.Monotone_to_LowerTopology_Continuous

added theorem LowerSetTopology.isOpen_iff_isLowerSet

added theorem LowerSetTopology.lowerSet_LE_lower

added theorem LowerSetTopology.monotone_to_lowerTopology_continuous

deleted def UpperLowerSet_toOrderDualHomeomorph

deleted theorem UpperSetDual_iff_LowerSet

deleted theorem UpperSetTopology.IsOpen_iff_IsUpperSet

deleted theorem UpperSetTopology.Monotone_to_UpperTopology_Continuous

deleted theorem UpperSetTopology.UpperSetLEUpper

added theorem UpperSetTopology.isOpen_iff_isUpperSet

added theorem UpperSetTopology.monotone_to_upperTopology_continuous

added theorem UpperSetTopology.upperSet_LE_upper

added def WithUpperSetTopology.toDualHomeomorph

added theorem lowerSet_dual_iff_upperSet

added theorem upperSet_dual_iff_lowerSet