Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-14 13:04 adfe9c7f

View on Github →

feat(topology/algebra/order/compact): Sup is continuous (#13347)

Prove that the Sup of a binary function over a compact set is continuous in the second variable
Some other lemmas about Sup
Move and generalize is_compact.bdd_[above|below]_image
from the sphere eversion project

Estimated changes

Modified src/topology/algebra/order/basic.lean

added theorem is_compact.bdd_above_image

added theorem is_compact.bdd_below_image

Modified src/topology/algebra/order/compact.lean

added theorem is_compact.Sup_lt_iff_of_continuous

deleted theorem is_compact.bdd_above_image

deleted theorem is_compact.bdd_below_image

added theorem is_compact.continuous_Inf

added theorem is_compact.continuous_Sup

added theorem is_compact.exists_Inf_image_eq_and_le

added theorem is_compact.exists_Sup_image_eq_and_ge

added theorem is_compact.lt_Inf_iff_of_continuous