Commit 2023-02-06 14:53 b9b1e2f2

View on Github →

feat: port Topology.Algebra.Order.Compact (#2089)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Bounds/Basic.lean

added theorem IsGreatest.lt_iff

added theorem IsLeast.lt_iff

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

added theorem CompactIccSpace.mk''

added theorem CompactIccSpace.mk'

added theorem Continuous.exists_forall_ge'

added theorem Continuous.exists_forall_ge

added theorem Continuous.exists_forall_ge_of_hasCompactMulSupport

added theorem Continuous.exists_forall_le'

added theorem Continuous.exists_forall_le

added theorem Continuous.exists_forall_le_of_hasCompactMulSupport

added theorem ContinuousOn.exists_forall_ge'

added theorem ContinuousOn.exists_forall_le'

added theorem ContinuousOn.exists_isMaxOn'

added theorem ContinuousOn.exists_isMinOn'

added theorem ContinuousOn.image_Icc

added theorem ContinuousOn.image_uIcc

added theorem ContinuousOn.image_uIcc_eq_Icc

added theorem ContinuousOn.infₛ_image_Icc_le

added theorem ContinuousOn.le_supₛ_image_Icc

added theorem IsCompact.continuous_infₛ

added theorem IsCompact.continuous_supₛ

added theorem IsCompact.exists_forall_ge

added theorem IsCompact.exists_forall_le

added theorem IsCompact.exists_infₛ_image_eq

added theorem IsCompact.exists_infₛ_image_eq_and_le

added theorem IsCompact.exists_isGLB

added theorem IsCompact.exists_isGreatest

added theorem IsCompact.exists_isLUB

added theorem IsCompact.exists_isLeast

added theorem IsCompact.exists_isLocalMinOn_mem_subset

added theorem IsCompact.exists_isMaxOn

added theorem IsCompact.exists_isMinOn

added theorem IsCompact.exists_isMinOn_mem_subset

added theorem IsCompact.exists_local_min_mem_open

added theorem IsCompact.exists_supₛ_image_eq

added theorem IsCompact.exists_supₛ_image_eq_and_ge

added theorem IsCompact.infₛ_mem

added theorem IsCompact.isGLB_infₛ

added theorem IsCompact.isGreatest_supₛ

added theorem IsCompact.isLUB_supₛ

added theorem IsCompact.isLeast_infₛ

added theorem IsCompact.lt_infₛ_iff_of_continuous

added theorem IsCompact.supₛ_lt_iff_of_continuous

added theorem IsCompact.supₛ_mem

added theorem eq_Icc_of_connected_compact

added theorem isCompact_uIcc