Commit 2023-08-15 16:57 b5ece309

View on Github →

feat: weaken assumptions for IsCompact.existsIsLeast and all of its variations (#6345) As discussed a while ago on Zulip, we introduce classes expressing that a certain topology has closed Icis/Iics, which is sufficient to get boundedness of compacts on the desired side. The main application is that these now apply to types satisfying UpperTopology/LowerTopology, which will allow us to apply these compactness results to semicontinuous functions. The naming was discussed here

Estimated changes

Modified Mathlib/Topology/Algebra/Order/Compact.lean

modified theorem Continuous.bddAbove_range_of_hasCompactMulSupport

modified theorem Continuous.bddBelow_range_of_hasCompactMulSupport

modified theorem Continuous.exists_forall_ge'

modified theorem Continuous.exists_forall_ge

modified theorem Continuous.exists_forall_ge_of_hasCompactMulSupport

modified theorem Continuous.exists_forall_le'

modified theorem Continuous.exists_forall_le

modified theorem Continuous.exists_forall_le_of_hasCompactMulSupport

modified theorem ContinuousOn.exists_forall_ge'

modified theorem ContinuousOn.exists_forall_le'

modified theorem ContinuousOn.exists_isMaxOn'

modified theorem ContinuousOn.exists_isMinOn'

modified theorem IsCompact.bddAbove

modified theorem IsCompact.bddAbove_image

modified theorem IsCompact.bddBelow

modified theorem IsCompact.bddBelow_image

modified theorem IsCompact.exists_forall_ge

modified theorem IsCompact.exists_forall_le

modified theorem IsCompact.exists_isGLB

modified theorem IsCompact.exists_isGreatest

modified theorem IsCompact.exists_isLUB

modified theorem IsCompact.exists_isLeast

added theorem IsCompact.exists_isLocalMax_mem_open

modified theorem IsCompact.exists_isLocalMinOn_mem_subset

modified theorem IsCompact.exists_isLocalMin_mem_open

modified theorem IsCompact.exists_isMaxOn

added theorem IsCompact.exists_isMaxOn_mem_subset

modified theorem IsCompact.exists_isMinOn

modified theorem IsCompact.exists_isMinOn_mem_subset

modified theorem IsCompact.exists_sInf_image_eq

modified theorem IsCompact.exists_sInf_image_eq_and_le

modified theorem IsCompact.exists_sSup_image_eq

modified theorem IsCompact.exists_sSup_image_eq_and_ge

modified theorem IsCompact.isGLB_sInf

modified theorem IsCompact.isGreatest_sSup

modified theorem IsCompact.isLUB_sSup

modified theorem IsCompact.isLeast_sInf

modified theorem IsCompact.lt_sInf_iff_of_continuous

modified theorem IsCompact.sInf_mem

modified theorem IsCompact.sSup_lt_iff_of_continuous

modified theorem IsCompact.sSup_mem

Modified Mathlib/Topology/Order/Basic.lean

deleted theorem isClosed_ge'

deleted theorem isClosed_le'

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

deleted theorem LowerTopology.isClosed_Ici

deleted theorem UpperTopology.isClosed_Iic