# Documentation

Mathlib.Topology.Algebra.Order.Compact

# Compactness of a closed interval #

In this file we prove that a closed interval in a conditionally complete linear ordered type with order topology (or a product of such types) is compact.

We prove the extreme value theorem (IsCompact.exists_isMinOn, IsCompact.exists_isMaxOn): a continuous function on a compact set takes its minimum and maximum values. We provide many variations of this theorem.

We also prove that the image of a closed interval under a continuous map is a closed interval, see ContinuousOn.image_Icc.

## Tags #

compact, extreme value theorem

### Compactness of a closed interval #

In this section we define a typeclass CompactIccSpace α saying that all closed intervals in α are compact. Then we provide an instance for a ConditionallyCompleteLinearOrder and prove that the product (both α × β and an indexed product) of spaces with this property inherits the property.

We also prove some simple lemmas about spaces with this property.

class CompactIccSpace (α : Type u_1) [] [] :
• isCompact_Icc : ∀ {a b : α}, IsCompact (Set.Icc a b)

A closed interval Set.Icc a b is a compact set for all a and b.

This typeclass says that all closed intervals in α are compact. This is true for all conditionally complete linear orders with order topology and products (finite or infinite) of such spaces.

Instances
theorem CompactIccSpace.mk' {α : Type u_1} [] [] (h : ∀ {a b : α}, a bIsCompact (Set.Icc a b)) :
theorem CompactIccSpace.mk'' {α : Type u_1} [] [] (h : ∀ {a b : α}, a < bIsCompact (Set.Icc a b)) :

A closed interval in a conditionally complete linear order is compact.

instance instCompactIccSpaceForAllTopologicalSpacePreorder {ι : Type u_1} {α : ιType u_2} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), CompactIccSpace (α i)] :
CompactIccSpace ((i : ι) → α i)
instance Pi.compact_Icc_space' {α : Type u_1} {β : Type u_2} [] [] [] :
CompactIccSpace (αβ)
theorem isCompact_uIcc {α : Type u_1} [] [] [] {a : α} {b : α} :

An unordered closed interval is compact.

instance compactSpace_of_completeLinearOrder {α : Type u_1} [] [] :

A complete linear order is a compact space.

We do not register an instance for a [CompactIccSpace α] because this would only add instances for products (indexed or not) of complete linear orders, and we have instances with higher priority that cover these cases.

instance compactSpace_Icc {α : Type u_1} [] [] [] (a : α) (b : α) :

### Extreme value theorem #

theorem IsCompact.exists_isLeast {α : Type u_1} [] [] {s : Set α} (hs : ) (ne_s : ) :
x, IsLeast s x
theorem IsCompact.exists_isGreatest {α : Type u_1} [] [] {s : Set α} (hs : ) (ne_s : ) :
x,
theorem IsCompact.exists_isGLB {α : Type u_1} [] [] {s : Set α} (hs : ) (ne_s : ) :
x, x s IsGLB s x
theorem IsCompact.exists_isLUB {α : Type u_1} [] [] {s : Set α} (hs : ) (ne_s : ) :
x, x s IsLUB s x
theorem IsCompact.exists_isMinOn {α : Type u_1} {β : Type u_2} [] [] [] {s : Set β} (hs : ) (ne_s : ) {f : βα} (hf : ) :
x, x s IsMinOn f s x

The extreme value theorem: a continuous function realizes its minimum on a compact set.

@[deprecated IsCompact.exists_isMinOn]
theorem IsCompact.exists_forall_le {α : Type u_1} {β : Type u_2} [] [] [] {s : Set β} (hs : ) (ne_s : ) {f : βα} (hf : ) :
x, x s ∀ (y : β), y sf x f y

The extreme value theorem: a continuous function realizes its minimum on a compact set.

theorem IsCompact.exists_isMaxOn {α : Type u_1} {β : Type u_2} [] [] [] {s : Set β} (hs : ) (ne_s : ) {f : βα} (hf : ) :
x, x s IsMaxOn f s x

The extreme value theorem: a continuous function realizes its maximum on a compact set.

@[deprecated IsCompact.exists_isMaxOn]
theorem IsCompact.exists_forall_ge {α : Type u_1} {β : Type u_2} [] [] [] {s : Set β} (hs : ) (ne_s : ) {f : βα} (hf : ) :
x, x s ∀ (y : β), y sf y f x

The extreme value theorem: a continuous function realizes its maximum on a compact set.

theorem ContinuousOn.exists_isMinOn' {α : Type u_1} {β : Type u_2} [] [] [] {s : Set β} {f : βα} (hf : ) (hsc : ) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x₀ f x) :
x, x s IsMinOn f s x

The extreme value theorem: if a function f is continuous on a closed set s and it is larger than a value in its image away from compact sets, then it has a minimum on this set.

@[deprecated ContinuousOn.exists_isMinOn']
theorem ContinuousOn.exists_forall_le' {α : Type u_1} {β : Type u_2} [] [] [] {s : Set β} {f : βα} (hf : ) (hsc : ) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x₀ f x) :
x, x s ∀ (y : β), y sf x f y

The extreme value theorem: if a function f is continuous on a closed set s and it is larger than a value in its image away from compact sets, then it has a minimum on this set.

theorem ContinuousOn.exists_isMaxOn' {α : Type u_1} {β : Type u_2} [] [] [] {s : Set β} {f : βα} (hf : ) (hsc : ) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x f x₀) :
x, x s IsMaxOn f s x

The extreme value theorem: if a function f is continuous on a closed set s and it is smaller than a value in its image away from compact sets, then it has a maximum on this set.

@[deprecated ContinuousOn.exists_isMaxOn']
theorem ContinuousOn.exists_forall_ge' {α : Type u_1} {β : Type u_2} [] [] [] {s : Set β} {f : βα} (hf : ) (hsc : ) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x f x₀) :
x, x s ∀ (y : β), y sf y f x

The extreme value theorem: if a function f is continuous on a closed set s and it is smaller than a value in its image away from compact sets, then it has a maximum on this set.

theorem Continuous.exists_forall_le' {α : Type u_1} {β : Type u_2} [] [] [] {f : βα} (hf : ) (x₀ : β) (h : ∀ᶠ (x : β) in , f x₀ f x) :
x, ∀ (y : β), f x f y

The extreme value theorem: if a continuous function f is larger than a value in its range away from compact sets, then it has a global minimum.

theorem Continuous.exists_forall_ge' {α : Type u_1} {β : Type u_2} [] [] [] {f : βα} (hf : ) (x₀ : β) (h : ∀ᶠ (x : β) in , f x f x₀) :
x, ∀ (y : β), f y f x

The extreme value theorem: if a continuous function f is smaller than a value in its range away from compact sets, then it has a global maximum.

theorem Continuous.exists_forall_le {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} (hf : ) (hlim : Filter.Tendsto f () Filter.atTop) :
x, ∀ (y : β), f x f y

The extreme value theorem: if a continuous function f tends to infinity away from compact sets, then it has a global minimum.

theorem Continuous.exists_forall_ge {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} (hf : ) (hlim : Filter.Tendsto f () Filter.atBot) :
x, ∀ (y : β), f y f x

The extreme value theorem: if a continuous function f tends to negative infinity away from compact sets, then it has a global maximum.

theorem Continuous.exists_forall_le_of_hasCompactSupport {α : Type u_1} {β : Type u_2} [] [] [] [] [Zero α] {f : βα} (hf : ) (h : ) :
x, ∀ (y : β), f x f y

A continuous function with compact support has a global minimum.

theorem Continuous.exists_forall_le_of_hasCompactMulSupport {α : Type u_1} {β : Type u_2} [] [] [] [] [One α] {f : βα} (hf : ) (h : ) :
x, ∀ (y : β), f x f y

A continuous function with compact support has a global minimum.

theorem Continuous.exists_forall_ge_of_hasCompactSupport {α : Type u_1} {β : Type u_2} [] [] [] [] [Zero α] {f : βα} (hf : ) (h : ) :
x, ∀ (y : β), f y f x

A continuous function with compact support has a global maximum.

theorem Continuous.exists_forall_ge_of_hasCompactMulSupport {α : Type u_1} {β : Type u_2} [] [] [] [] [One α] {f : βα} (hf : ) (h : ) :
x, ∀ (y : β), f y f x

A continuous function with compact support has a global maximum.

theorem IsCompact.bddBelow {α : Type u_1} [] [] [] {s : Set α} (hs : ) :

A compact set is bounded below

theorem IsCompact.bddAbove {α : Type u_1} [] [] [] {s : Set α} (hs : ) :

A compact set is bounded above

theorem IsCompact.bddBelow_image {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} {K : Set β} (hK : ) (hf : ) :
BddBelow (f '' K)

A continuous function is bounded below on a compact set.

theorem IsCompact.bddAbove_image {α : Type u_1} {β : Type u_2} [] [] [] [] {f : βα} {K : Set β} (hK : ) (hf : ) :
BddAbove (f '' K)

A continuous function is bounded above on a compact set.

theorem Continuous.bddBelow_range_of_hasCompactSupport {α : Type u_1} {β : Type u_2} [] [] [] [Zero α] {f : βα} (hf : ) (h : ) :

A continuous function with compact support is bounded below.

theorem Continuous.bddBelow_range_of_hasCompactMulSupport {α : Type u_1} {β : Type u_2} [] [] [] [One α] {f : βα} (hf : ) (h : ) :

A continuous function with compact support is bounded below.

theorem Continuous.bddAbove_range_of_hasCompactSupport {α : Type u_1} {β : Type u_2} [] [] [] [Zero α] {f : βα} (hf : ) (h : ) :

A continuous function with compact support is bounded above.

theorem Continuous.bddAbove_range_of_hasCompactMulSupport {α : Type u_1} {β : Type u_2} [] [] [] [One α] {f : βα} (hf : ) (h : ) :

A continuous function with compact support is bounded above.

theorem IsCompact.sSup_lt_iff_of_continuous {α : Type u_1} {β : Type u_2} [] [] {f : βα} {K : Set β} (hK : ) (h0K : ) (hf : ) (y : α) :
sSup (f '' K) < y ∀ (x : β), x Kf x < y
theorem IsCompact.lt_sInf_iff_of_continuous {α : Type u_1} {β : Type u_2} [] [] {f : βα} {K : Set β} (hK : ) (h0K : ) (hf : ) (y : α) :
y < sInf (f '' K) ∀ (x : β), x Ky < f x

### Min and max elements of a compact set #

theorem IsCompact.sInf_mem {α : Type u_1} [] {s : Set α} (hs : ) (ne_s : ) :
sInf s s
theorem IsCompact.sSup_mem {α : Type u_1} [] {s : Set α} (hs : ) (ne_s : ) :
sSup s s
theorem IsCompact.isGLB_sInf {α : Type u_1} [] {s : Set α} (hs : ) (ne_s : ) :
IsGLB s (sInf s)
theorem IsCompact.isLUB_sSup {α : Type u_1} [] {s : Set α} (hs : ) (ne_s : ) :
IsLUB s (sSup s)
theorem IsCompact.isLeast_sInf {α : Type u_1} [] {s : Set α} (hs : ) (ne_s : ) :
theorem IsCompact.isGreatest_sSup {α : Type u_1} [] {s : Set α} (hs : ) (ne_s : ) :
theorem IsCompact.exists_sInf_image_eq_and_le {α : Type u_1} {β : Type u_2} [] [] {s : Set β} (hs : ) (ne_s : ) {f : βα} (hf : ) :
x, x s sInf (f '' s) = f x ∀ (y : β), y sf x f y
theorem IsCompact.exists_sSup_image_eq_and_ge {α : Type u_1} {β : Type u_2} [] [] {s : Set β} (hs : ) (ne_s : ) {f : βα} (hf : ) :
x, x s sSup (f '' s) = f x ∀ (y : β), y sf y f x
theorem IsCompact.exists_sInf_image_eq {α : Type u_1} {β : Type u_2} [] [] {s : Set β} (hs : ) (ne_s : ) {f : βα} (hf : ) :
x, x s sInf (f '' s) = f x
theorem IsCompact.exists_sSup_image_eq {α : Type u_1} {β : Type u_2} [] [] {s : Set β} (hs : ) (ne_s : ) {f : βα} :
x, x s sSup (f '' s) = f x
theorem IsCompact.exists_isMinOn_mem_subset {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : ) (hf : ) (hz : z t) (hfz : ∀ (z' : β), z' t \ sf z < f z') :
x, x s IsMinOn f t x
theorem IsCompact.exists_isMaxOn_mem_subset {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : ) (hf : ) (hz : z t) (hfz : ∀ (z' : β), z' t \ sf z' < f z) :
x, x s IsMaxOn f t x
@[deprecated IsCompact.exists_isMinOn_mem_subset]
theorem IsCompact.exists_isLocalMinOn_mem_subset {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : ) (hf : ) (hz : z t) (hfz : ∀ (z' : β), z' t \ sf z < f z') :
x, x s IsLocalMinOn f t x
theorem IsCompact.exists_isLocalMin_mem_open {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : ) (hst : s t) (hf : ) (hz : z t) (hfz : ∀ (z' : β), z' t \ sf z < f z') (hs : ) :
x, x s
theorem IsCompact.exists_isLocalMax_mem_open {α : Type u_1} {β : Type u_2} [] [] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : ) (hst : s t) (hf : ) (hz : z t) (hfz : ∀ (z' : β), z' t \ sf z' < f z) (hs : ) :
x, x s
theorem eq_Icc_of_connected_compact {α : Type u_1} [] [] {s : Set α} (h₁ : ) (h₂ : ) :
s = Set.Icc (sInf s) (sSup s)
theorem IsCompact.continuous_sSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : γβα} {K : Set β} (hK : ) (hf : ) :
Continuous fun x => sSup (f x '' K)
theorem IsCompact.continuous_sInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : γβα} {K : Set β} (hK : ) (hf : ) :
Continuous fun x => sInf (f x '' K)

### Image of a closed interval #

theorem ContinuousOn.image_Icc {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} {a : α} {b : α} (hab : a b) (h : ContinuousOn f (Set.Icc a b)) :
f '' Set.Icc a b = Set.Icc (sInf (f '' Set.Icc a b)) (sSup (f '' Set.Icc a b))
theorem ContinuousOn.image_uIcc_eq_Icc {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} {a : α} {b : α} (h : ContinuousOn f (Set.uIcc a b)) :
f '' Set.uIcc a b = Set.Icc (sInf (f '' Set.uIcc a b)) (sSup (f '' Set.uIcc a b))
theorem ContinuousOn.image_uIcc {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} {a : α} {b : α} (h : ContinuousOn f (Set.uIcc a b)) :
f '' Set.uIcc a b = Set.uIcc (sInf (f '' Set.uIcc a b)) (sSup (f '' Set.uIcc a b))
theorem ContinuousOn.sInf_image_Icc_le {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} {a : α} {b : α} {c : α} (h : ContinuousOn f (Set.Icc a b)) (hc : c Set.Icc a b) :
sInf (f '' Set.Icc a b) f c
theorem ContinuousOn.le_sSup_image_Icc {α : Type u_1} {β : Type u_2} [] [] [] [] [] {f : αβ} {a : α} {b : α} {c : α} (h : ContinuousOn f (Set.Icc a b)) (hc : c Set.Icc a b) :
f c sSup (f '' Set.Icc a b)