# 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) [] [] :

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.

• 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.

Instances
theorem CompactIccSpace.isCompact_Icc {α : Type u_1} [] [] [self : ] {a : α} {b : α} :

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

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)) :
instance instCompactIccSpaceOrderDual {α : Type u_1} [] [] [] :
Equations
• =
@[instance 100]

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

Equations
• =
instance instCompactIccSpaceForall {ι : Type u_2} {α : ιType u_3} [(i : ι) → Preorder (α i)] [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), CompactIccSpace (α i)] :
CompactIccSpace ((i : ι) → α i)
Equations
• =
instance Pi.compact_Icc_space' {α : Type u_2} {β : Type u_3} [] [] [] :
CompactIccSpace (αβ)
Equations
• =
instance instCompactIccSpaceProd {α : Type u_2} {β : Type u_3} [] [] [] [] [] [] :
Equations
• =
theorem isCompact_uIcc {α : Type u_2} [] [] [] {a : α} {b : α} :

An unordered closed interval is compact.

@[instance 100]
instance compactSpace_of_completeLinearOrder {α : Type u_2} [] [] :

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.

Equations
• =
instance compactSpace_Icc {α : Type u_2} [] [] [] (a : α) (b : α) :
Equations
• =

### Extreme value theorem #

theorem IsCompact.exists_isLeast {α : Type u_2} [] [] {s : Set α} (hs : ) (ne_s : s.Nonempty) :
∃ (x : α), IsLeast s x
theorem IsCompact.exists_isGreatest {α : Type u_2} [] [] {s : Set α} (hs : ) (ne_s : s.Nonempty) :
∃ (x : α),
theorem IsCompact.exists_isGLB {α : Type u_2} [] [] {s : Set α} (hs : ) (ne_s : s.Nonempty) :
xs, IsGLB s x
theorem IsCompact.exists_isLUB {α : Type u_2} [] [] {s : Set α} (hs : ) (ne_s : s.Nonempty) :
xs, IsLUB s x
theorem cocompact_le_atBot_atTop {α : Type u_2} [] [] [] :
Filter.atBot Filter.atTop
theorem cocompact_le_atBot {α : Type u_2} [] [] [] [] :
Filter.atBot
theorem cocompact_le_atTop {α : Type u_2} [] [] [] [] :
Filter.atTop
theorem atBot_le_cocompact {α : Type u_2} [] [] [] :
Filter.atBot
theorem atTop_le_cocompact {α : Type u_2} [] [] [] :
Filter.atTop
theorem atBot_atTop_le_cocompact {α : Type u_2} [] [] [] [] :
Filter.atBot Filter.atTop
@[simp]
theorem cocompact_eq_atBot_atTop {α : Type u_2} [] [] [] [] [] :
= Filter.atBot Filter.atTop
@[simp]
theorem cocompact_eq_atBot {α : Type u_2} [] [] [] [] [] :
= Filter.atBot
@[simp]
theorem cocompact_eq_atTop {α : Type u_2} [] [] [] [] [] :
= Filter.atTop
theorem IsCompact.exists_isMinOn {α : Type u_2} {β : Type u_3} [] [] [] {s : Set β} (hs : ) (ne_s : s.Nonempty) {f : βα} (hf : ) :
xs, IsMinOn f s x

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

theorem IsCompact.exists_forall_le' {α : Type u_2} {β : Type u_3} [] [] [] [] {f : βα} {s : Set β} (hs : ) (hf : ) {a : α} (hf' : bs, a < f b) :
∃ (a' : α), a < a' bs, a' f b

If a continuous function lies strictly above a on a compact set, it has a lower bound strictly above a.

@[deprecated IsCompact.exists_isMinOn]
theorem IsCompact.exists_forall_le {α : Type u_2} {β : Type u_3} [] [] [] {s : Set β} (hs : ) (ne_s : s.Nonempty) {f : βα} (hf : ) :
xs, ys, f x f y

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

theorem IsCompact.exists_isMaxOn {α : Type u_2} {β : Type u_3} [] [] [] {s : Set β} (hs : ) (ne_s : s.Nonempty) {f : βα} (hf : ) :
xs, 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_2} {β : Type u_3} [] [] [] {s : Set β} (hs : ) (ne_s : s.Nonempty) {f : βα} (hf : ) :
xs, ys, f y f x

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

theorem ContinuousOn.exists_isMinOn' {α : Type u_2} {β : Type u_3} [] [] [] {s : Set β} {f : βα} (hf : ) (hsc : ) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x₀ f x) :
xs, 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_2} {β : Type u_3} [] [] [] {s : Set β} {f : βα} (hf : ) (hsc : ) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x₀ f x) :
xs, ys, f 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_2} {β : Type u_3} [] [] [] {s : Set β} {f : βα} (hf : ) (hsc : ) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x f x₀) :
xs, 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_2} {β : Type u_3} [] [] [] {s : Set β} {f : βα} (hf : ) (hsc : ) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x f x₀) :
xs, ys, f 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_2} {β : Type u_3} [] [] [] {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_2} {β : Type u_3} [] [] [] {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_2} {β : Type u_3} [] [] [] [] {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_2} {β : Type u_3} [] [] [] [] {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_2} {β : Type u_3} [] [] [] [] [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_2} {β : Type u_3} [] [] [] [] [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_2} {β : Type u_3} [] [] [] [] [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_2} {β : Type u_3} [] [] [] [] [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_2} [] [] [] {s : Set α} (hs : ) :

A compact set is bounded below

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

A compact set is bounded above

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

A continuous function is bounded below on a compact set.

theorem IsCompact.bddAbove_image {α : Type u_2} {β : Type u_3} [] [] [] [] {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_2} {β : Type u_3} [] [] [] [Zero α] {f : βα} (hf : ) (h : ) :

A continuous function with compact support is bounded below.

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

A continuous function with compact support is bounded below.

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

A continuous function with compact support is bounded above.

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

A continuous function with compact support is bounded above.

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

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

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

If f : γ → β → α is a function that is continuous as a function on γ × β, α is a conditionally complete linear order, and K : Set β is a compact set, then fun x ↦ sSup (f x '' K) is a continuous function.

theorem IsCompact.continuous_sInf {α : Type u_2} {β : Type u_3} {γ : Type u_4} [] [] [] [] {f : γβα} {K : Set β} (hK : ) (hf : ) :
Continuous fun (x : γ) => sInf (f x '' K)

### Image of a closed interval #

theorem ContinuousOn.image_Icc {α : Type u_2} {β : Type u_3} [] [] [] [] [] {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_2} {β : Type u_3} [] [] [] [] [] {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_2} {β : Type u_3} [] [] [] [] [] {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_2} {β : Type u_3} [] [] [] [] [] {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_2} {β : Type u_3} [] [] [] [] [] {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)