Commit 2023-09-24 19:47 6a6a3a83

View on Github →

refactor(Topology/Order): Rename order topologies (#7310) Rename the Upper/Lower UpperSet/LowerSet topologies to the conventions suggested by @YaelDillies in https://github.com/leanprover-community/mathlib4/pull/2508#discussion_r1306711450

Estimated changes

Modified Mathlib/Topology/Order/Category/AlexDisc.lean

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

deleted theorem LowerTopology.closure_singleton

deleted theorem LowerTopology.continuous_of_Ici

deleted theorem LowerTopology.isClosed_upperClosure

deleted theorem LowerTopology.isLowerSet_of_isOpen

deleted theorem LowerTopology.isOpen_iff_generate_Ici_compl

deleted theorem LowerTopology.isUpperSet_of_isClosed

deleted def LowerTopology.lowerBasis

deleted theorem LowerTopology.topology_eq

deleted def LowerTopology.withLowerTopologyHomeomorph

added def Topology.IsLower.WithLowerHomeomorph

added theorem Topology.IsLower.closure_singleton

added theorem Topology.IsLower.continuous_of_Ici

added theorem Topology.IsLower.isClosed_upperClosure

added theorem Topology.IsLower.isLowerSet_of_isOpen

added theorem Topology.IsLower.isOpen_iff_generate_Ici_compl

added theorem Topology.IsLower.isUpperSet_of_isClosed

added def Topology.IsLower.lowerBasis

added theorem Topology.IsLower.topology_eq

added def Topology.IsUpper.WithUpperHomeomorph

added theorem Topology.IsUpper.closure_singleton

added theorem Topology.IsUpper.continuous_of_Iic

added theorem Topology.IsUpper.isClosed_lowerClosure

added theorem Topology.IsUpper.isLowerSet_of_isClosed

added theorem Topology.IsUpper.isOpen_iff_generate_Iic_compl

added theorem Topology.IsUpper.isUpperSet_of_isOpen

added theorem Topology.IsUpper.topology_eq

added def Topology.IsUpper.upperBasis

added theorem Topology.WithLower.isOpen_def

added theorem Topology.WithLower.isOpen_preimage_ofLower

added def Topology.WithLower.ofLower

added theorem Topology.WithLower.ofLower_inj

added theorem Topology.WithLower.ofLower_toLower

added theorem Topology.WithLower.of_WithLower_symm_eq

added def Topology.WithLower.toDualHomeomorph

added def Topology.WithLower.toLower

added theorem Topology.WithLower.toLower_inj

added theorem Topology.WithLower.toLower_ofLower

added theorem Topology.WithLower.to_WithLower_symm_eq

added def Topology.WithLower

added theorem Topology.WithUpper.isOpen_def

added theorem Topology.WithUpper.isOpen_preimage_ofUpper

added def Topology.WithUpper.ofUpper

added theorem Topology.WithUpper.ofUpper_inj

added theorem Topology.WithUpper.ofUpper_toUpper

added theorem Topology.WithUpper.of_WithUpper_symm_eq

added def Topology.WithUpper.toUpper

added theorem Topology.WithUpper.toUpper_inj

added theorem Topology.WithUpper.toUpper_ofUpper

added theorem Topology.WithUpper.to_WithUpper_symm_eq

added def Topology.WithUpper

added theorem Topology.isLower_orderDual

added theorem Topology.isUpper_orderDual

added def Topology.lower

added def Topology.upper

deleted theorem UpperTopology.closure_singleton

deleted theorem UpperTopology.continuous_of_Iic

deleted theorem UpperTopology.isClosed_lowerClosure

deleted theorem UpperTopology.isLowerSet_of_isClosed

deleted theorem UpperTopology.isOpen_iff_generate_Iic_compl

deleted theorem UpperTopology.isUpperSet_of_isOpen

deleted theorem UpperTopology.topology_eq

deleted def UpperTopology.upperBasis

deleted def UpperTopology.withUpperTopologyHomeomorph

deleted theorem WithLowerTopology.isOpen_def

deleted theorem WithLowerTopology.isOpen_preimage_ofLower

deleted def WithLowerTopology.ofLower

deleted theorem WithLowerTopology.ofLower_inj

deleted theorem WithLowerTopology.ofLower_toLower

deleted theorem WithLowerTopology.of_withLowerTopology_symm_eq

deleted def WithLowerTopology.toDualHomeomorph

deleted def WithLowerTopology.toLower

deleted theorem WithLowerTopology.toLower_inj

deleted theorem WithLowerTopology.toLower_ofLower

deleted theorem WithLowerTopology.to_withLowerTopology_symm_eq

deleted def WithLowerTopology

deleted theorem WithUpperTopology.isOpen_def

deleted theorem WithUpperTopology.isOpen_preimage_ofUpper

deleted def WithUpperTopology.ofUpper

deleted theorem WithUpperTopology.ofUpper_inj

deleted theorem WithUpperTopology.ofUpper_toUpper

deleted theorem WithUpperTopology.of_withUpperTopology_symm_eq

deleted def WithUpperTopology.toUpper

deleted theorem WithUpperTopology.toUpper_inj

deleted theorem WithUpperTopology.toUpper_ofUpper

deleted theorem WithUpperTopology.to_withUpperTopology_symm_eq

deleted def WithUpperTopology

deleted theorem lower_dual_iff_upper

deleted theorem upper_dual_iff_lower

Modified Mathlib/Topology/Order/UpperLowerSetTopology.lean

deleted theorem LowerSetTopology.closure_eq_upperClosure

deleted theorem LowerSetTopology.closure_singleton

deleted theorem LowerSetTopology.isClosed_iff_isUpper

deleted theorem LowerSetTopology.isClosed_isUpper

deleted theorem LowerSetTopology.isOpen_iff_isLowerSet

deleted theorem LowerSetTopology.lowerSet_LE_lower

deleted theorem LowerSetTopology.monotone_to_lowerTopology_continuous

deleted theorem LowerSetTopology.topology_eq

deleted def LowerSetTopology.withLowerSetTopologyHomeomorph

added def Topology.IsLowerSet.WithLowerSetHomeomorph

added theorem Topology.IsLowerSet.closure_eq_upperClosure

added theorem Topology.IsLowerSet.closure_singleton

added theorem Topology.IsLowerSet.isClosed_iff_isUpper

added theorem Topology.IsLowerSet.isOpen_iff_isLowerSet

added theorem Topology.IsLowerSet.lowerSet_le_lower

added theorem Topology.IsLowerSet.monotone_to_lowerTopology_continuous

added theorem Topology.IsLowerSet.topology_eq

added def Topology.IsUpperSet.WithUpperSetHomeomorph

added theorem Topology.IsUpperSet.closure_eq_lowerClosure

added theorem Topology.IsUpperSet.closure_singleton

added theorem Topology.IsUpperSet.isClosed_iff_isLower

added theorem Topology.IsUpperSet.isOpen_iff_isUpperSet

added theorem Topology.IsUpperSet.monotone_to_upperTopology_continuous

added theorem Topology.IsUpperSet.topology_eq

added theorem Topology.IsUpperSet.upperSet_le_upper

added theorem Topology.WithLowerSet.isLowerSet_toLowerSet_preimage

added theorem Topology.WithLowerSet.isOpen_ofLowerSet_preimage

added def Topology.WithLowerSet.map

added theorem Topology.WithLowerSet.map_comp

added theorem Topology.WithLowerSet.map_id

added def Topology.WithLowerSet.ofLowerSet

added def Topology.WithLowerSet.ofLowerSetOrderIso

added theorem Topology.WithLowerSet.ofLowerSet_inj

added theorem Topology.WithLowerSet.ofLowerSet_le_iff

added theorem Topology.WithLowerSet.ofLowerSet_le_ofLowerSet

added theorem Topology.WithLowerSet.ofLowerSet_toLowerSet

added theorem Topology.WithLowerSet.of_WithLowerSet_symm_eq

added def Topology.WithLowerSet.toLowerSet

added def Topology.WithLowerSet.toLowerSetOrderIso

added theorem Topology.WithLowerSet.toLowerSet_inj

added theorem Topology.WithLowerSet.toLowerSet_le_iff

added theorem Topology.WithLowerSet.toLowerSet_ofLowerSet

added theorem Topology.WithLowerSet.toLowerSet_specializes_toLowerSet

added theorem Topology.WithLowerSet.to_WithLowerSet_symm_eq

added def Topology.WithLowerSet

added theorem Topology.WithUpperSet.isOpen_ofUpperSet_preimage

added theorem Topology.WithUpperSet.isUpperSet_toUpperSet_preimage

added def Topology.WithUpperSet.map

added theorem Topology.WithUpperSet.map_comp

added theorem Topology.WithUpperSet.map_id

added def Topology.WithUpperSet.ofUpperSet

added def Topology.WithUpperSet.ofUpperSetOrderIso

added theorem Topology.WithUpperSet.ofUpperSet_inj

added theorem Topology.WithUpperSet.ofUpperSet_le_iff

added theorem Topology.WithUpperSet.ofUpperSet_le_ofUpperSet

added theorem Topology.WithUpperSet.ofUpperSet_toUpperSet

added theorem Topology.WithUpperSet.of_WithUpperSet_symm_eq

added def Topology.WithUpperSet.toDualHomeomorph

added def Topology.WithUpperSet.toUpperSet

added def Topology.WithUpperSet.toUpperSetOrderIso

added theorem Topology.WithUpperSet.toUpperSet_inj

added theorem Topology.WithUpperSet.toUpperSet_le_iff

added theorem Topology.WithUpperSet.toUpperSet_ofUpperSet

added theorem Topology.WithUpperSet.toUpperSet_specializes_toUpperSet

added theorem Topology.WithUpperSet.to_WithUpperSet_symm_eq

added def Topology.WithUpperSet

added theorem Topology.isLowerSet_orderDual

added theorem Topology.isUpperSet_orderDual

added def Topology.lowerSet

added def Topology.upperSet

deleted theorem UpperSetTopology.closure_eq_lowerClosure

deleted theorem UpperSetTopology.closure_singleton

deleted theorem UpperSetTopology.isClosed_iff_isLower

deleted theorem UpperSetTopology.isClosed_isLower

deleted theorem UpperSetTopology.isOpen_iff_isUpperSet

deleted theorem UpperSetTopology.monotone_to_upperTopology_continuous

deleted theorem UpperSetTopology.topology_eq

deleted theorem UpperSetTopology.upperSet_LE_upper

deleted def UpperSetTopology.withUpperSetTopologyHomeomorph

deleted theorem WithLowerSetTopology.isLowerSet_toLowerSet_preimage

deleted theorem WithLowerSetTopology.isOpen_ofLowerSet_preimage

deleted def WithLowerSetTopology.map

deleted theorem WithLowerSetTopology.map_comp

deleted theorem WithLowerSetTopology.map_id

deleted def WithLowerSetTopology.ofLowerSet

deleted def WithLowerSetTopology.ofLowerSetOrderIso

deleted theorem WithLowerSetTopology.ofLowerSet_inj

deleted theorem WithLowerSetTopology.ofLowerSet_le_iff

deleted theorem WithLowerSetTopology.ofLowerSet_le_ofLowerSet

deleted theorem WithLowerSetTopology.ofLowerSet_toLowerSet

deleted theorem WithLowerSetTopology.of_withLowerSetTopology_symm_eq

deleted def WithLowerSetTopology.toLowerSet

deleted def WithLowerSetTopology.toLowerSetOrderIso

deleted theorem WithLowerSetTopology.toLowerSet_inj

deleted theorem WithLowerSetTopology.toLowerSet_le_iff

deleted theorem WithLowerSetTopology.toLowerSet_ofLowerSet

deleted theorem WithLowerSetTopology.toLowerSet_specializes_toLowerSet

deleted theorem WithLowerSetTopology.to_withLowerSetTopology_symm_eq

deleted def WithLowerSetTopology

deleted theorem WithUpperSetTopology.isOpen_ofUpperSet_preimage

deleted theorem WithUpperSetTopology.isUpperSet_toUpperSet_preimage

deleted def WithUpperSetTopology.map

deleted theorem WithUpperSetTopology.map_comp

deleted theorem WithUpperSetTopology.map_id

deleted def WithUpperSetTopology.ofUpperSet

deleted def WithUpperSetTopology.ofUpperSetOrderIso

deleted theorem WithUpperSetTopology.ofUpperSet_inj

deleted theorem WithUpperSetTopology.ofUpperSet_le_iff

deleted theorem WithUpperSetTopology.ofUpperSet_le_ofUpperSet

deleted theorem WithUpperSetTopology.ofUpperSet_toUpperSet

deleted theorem WithUpperSetTopology.of_withUpperSetTopology_symm_eq

deleted def WithUpperSetTopology.toDualHomeomorph

deleted def WithUpperSetTopology.toUpperSet

deleted def WithUpperSetTopology.toUpperSetOrderIso

deleted theorem WithUpperSetTopology.toUpperSet_inj

deleted theorem WithUpperSetTopology.toUpperSet_le_iff

deleted theorem WithUpperSetTopology.toUpperSet_ofUpperSet

deleted theorem WithUpperSetTopology.toUpperSet_specializes_toUpperSet

deleted theorem WithUpperSetTopology.to_withUpperSetTopology_symm_eq

deleted def WithUpperSetTopology

deleted def lowerSetTopology'

deleted theorem lowerSet_dual_iff_upperSet

deleted def upperSetTopology'

deleted theorem upperSet_dual_iff_lowerSet

Modified Mathlib/Topology/Specialization.lean