# mathlib3documentation

topology.algebra.order.compact

# Compactness of a closed interval #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (is_compact.exists_forall_le, is_compact.exists_forall_ge): 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 continuous_on.image_Icc.

## Tags #

compact, extreme value theorem

### Compactness of a closed interval #

In this section we define a typeclass compact_Icc_space α saying that all closed intervals in α are compact. Then we provide an instance for a conditionally_complete_linear_order 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]
structure compact_Icc_space (α : Type u_1) [preorder α] :
Prop

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 of this typeclass
@[protected, instance]

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

@[protected, instance]
def pi.compact_Icc_space {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), preorder (α i)] [Π (i : ι), topological_space (α i)] [ (i : ι), compact_Icc_space (α i)] :
compact_Icc_space (Π (i : ι), α i)
@[protected, instance]
def pi.compact_Icc_space' {α : Type u_1} {β : Type u_2} [preorder β]  :
@[protected, instance]
def prod.compact_Icc_space {α : Type u_1} {β : Type u_2} [preorder α] [preorder β]  :
theorem is_compact_uIcc {α : Type u_1} [linear_order α] {a b : α} :

An unordered closed interval is compact.

@[protected, instance]

A complete linear order is a compact space.

We do not register an instance for a [compact_Icc_space α] 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.

@[protected, instance]
def compact_space_Icc {α : Type u_1} [preorder α] (a b : α) :

### Extreme value theorem #

theorem is_compact.exists_is_least {α : Type u_1} [linear_order α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
(x : α), x
theorem is_compact.exists_is_greatest {α : Type u_1} [linear_order α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
(x : α), x
theorem is_compact.exists_is_glb {α : Type u_1} [linear_order α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
(x : α) (H : x s), x
theorem is_compact.exists_is_lub {α : Type u_1} [linear_order α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
(x : α) (H : x s), x
theorem is_compact.exists_forall_le {α : Type u_1} {β : Type u_2} [linear_order α] {s : set β} (hs : is_compact s) (ne_s : s.nonempty) {f : β α} (hf : s) :
(x : β) (H : x s), (y : β), y s f x f y

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

theorem is_compact.exists_forall_ge {α : Type u_1} {β : Type u_2} [linear_order α] {s : set β} :
s.nonempty {f : β α}, ( (x : β) (H : x s), (y : β), y s f y f x)

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

theorem continuous_on.exists_forall_le' {α : Type u_1} {β : Type u_2} [linear_order α] {s : set β} {f : β α} (hf : s) (hsc : is_closed s) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x₀ f x) :
(x : β) (H : x s), (y : β), y s 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 continuous_on.exists_forall_ge' {α : Type u_1} {β : Type u_2} [linear_order α] {s : set β} {f : β α} (hf : s) (hsc : is_closed s) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in , f x f x₀) :
(x : β) (H : x s), (y : β), y s 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_1} {β : Type u_2} [linear_order α] {f : β α} (hf : continuous f) (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} [linear_order α] {f : β α} (hf : continuous f) (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} [linear_order α] [nonempty β] {f : β α} (hf : continuous f) (hlim : filter.at_top) :
(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} [linear_order α] [nonempty β] {f : β α} (hf : continuous f) (hlim : filter.at_bot) :
(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_has_compact_support {α : Type u_1} {β : Type u_2} [linear_order α] [nonempty β] [has_zero α] {f : β α} (hf : continuous f) (h : has_compact_support f) :
(x : β), (y : β), f x f y

A continuous function with compact support has a global minimum.

theorem continuous.exists_forall_le_of_has_compact_mul_support {α : Type u_1} {β : Type u_2} [linear_order α] [nonempty β] [has_one α] {f : β α} (hf : continuous f) (h : has_compact_mul_support f) :
(x : β), (y : β), f x f y

A continuous function with compact support has a global minimum.

theorem continuous.exists_forall_ge_of_has_compact_mul_support {α : Type u_1} {β : Type u_2} [linear_order α] [nonempty β] [has_one α] {f : β α} (hf : continuous f) (h : has_compact_mul_support f) :
(x : β), (y : β), f y f x

A continuous function with compact support has a global maximum.

theorem continuous.exists_forall_ge_of_has_compact_support {α : Type u_1} {β : Type u_2} [linear_order α] [nonempty β] [has_zero α] {f : β α} (hf : continuous f) (h : has_compact_support f) :
(x : β), (y : β), f y f x

A continuous function with compact support has a global maximum.

theorem is_compact.bdd_below {α : Type u_1} [linear_order α] [nonempty α] {s : set α} (hs : is_compact s) :

A compact set is bounded below

theorem is_compact.bdd_above {α : Type u_1} [linear_order α] [nonempty α] {s : set α} (hs : is_compact s) :

A compact set is bounded above

theorem is_compact.bdd_below_image {α : Type u_1} {β : Type u_2} [linear_order α] [nonempty α] {f : β α} {K : set β} (hK : is_compact K) (hf : K) :

A continuous function is bounded below on a compact set.

theorem is_compact.bdd_above_image {α : Type u_1} {β : Type u_2} [linear_order α] [nonempty α] {f : β α} {K : set β} (hK : is_compact K) (hf : K) :

A continuous function is bounded above on a compact set.

theorem continuous.bdd_below_range_of_has_compact_mul_support {α : Type u_1} {β : Type u_2} [linear_order α] [has_one α] {f : β α} (hf : continuous f) (h : has_compact_mul_support f) :

A continuous function with compact support is bounded below.

theorem continuous.bdd_below_range_of_has_compact_support {α : Type u_1} {β : Type u_2} [linear_order α] [has_zero α] {f : β α} (hf : continuous f) (h : has_compact_support f) :

A continuous function with compact support is bounded below.

theorem continuous.bdd_above_range_of_has_compact_support {α : Type u_1} {β : Type u_2} [linear_order α] [has_zero α] {f : β α} (hf : continuous f) (h : has_compact_support f) :

A continuous function with compact support is bounded above.

theorem continuous.bdd_above_range_of_has_compact_mul_support {α : Type u_1} {β : Type u_2} [linear_order α] [has_one α] {f : β α} (hf : continuous f) (h : has_compact_mul_support f) :

A continuous function with compact support is bounded above.

theorem is_compact.Sup_lt_iff_of_continuous {α : Type u_1} {β : Type u_2} {f : β α} {K : set β} (hK : is_compact K) (h0K : K.nonempty) (hf : K) (y : α) :
has_Sup.Sup (f '' K) < y (x : β), x K f x < y
theorem is_compact.lt_Inf_iff_of_continuous {α : Type u_1} {β : Type u_2} {f : β α} {K : set β} (hK : is_compact K) (h0K : K.nonempty) (hf : K) (y : α) :
y < has_Inf.Inf (f '' K) (x : β), x K y < f x

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

theorem is_compact.Inf_mem {α : Type u_1} {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
s
theorem is_compact.Sup_mem {α : Type u_1} {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
s
theorem is_compact.is_glb_Inf {α : Type u_1} {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
theorem is_compact.is_lub_Sup {α : Type u_1} {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
theorem is_compact.is_least_Inf {α : Type u_1} {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
theorem is_compact.is_greatest_Sup {α : Type u_1} {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :
theorem is_compact.exists_Inf_image_eq_and_le {α : Type u_1} {β : Type u_2} {s : set β} (hs : is_compact s) (ne_s : s.nonempty) {f : β α} (hf : s) :
(x : β) (H : x s), has_Inf.Inf (f '' s) = f x (y : β), y s f x f y
theorem is_compact.exists_Sup_image_eq_and_ge {α : Type u_1} {β : Type u_2} {s : set β} (hs : is_compact s) (ne_s : s.nonempty) {f : β α} (hf : s) :
(x : β) (H : x s), has_Sup.Sup (f '' s) = f x (y : β), y s f y f x
theorem is_compact.exists_Inf_image_eq {α : Type u_1} {β : Type u_2} {s : set β} (hs : is_compact s) (ne_s : s.nonempty) {f : β α} (hf : s) :
(x : β) (H : x s), has_Inf.Inf (f '' s) = f x
theorem is_compact.exists_Sup_image_eq {α : Type u_1} {β : Type u_2} {s : set β} :
s.nonempty {f : β α}, ( (x : β) (H : x s), has_Sup.Sup (f '' s) = f x)
theorem eq_Icc_of_connected_compact {α : Type u_1} {s : set α} (h₁ : is_connected s) (h₂ : is_compact s) :
theorem is_compact.continuous_Sup {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γ β α} {K : set β} (hK : is_compact K) (hf : continuous f) :
continuous (λ (x : γ), has_Sup.Sup (f x '' K))
theorem is_compact.continuous_Inf {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γ β α} {K : set β} (hK : is_compact K) (hf : continuous f) :
continuous (λ (x : γ), has_Inf.Inf (f x '' K))

### Image of a closed interval #

theorem continuous_on.image_Icc {α : Type u_1} {β : Type u_2} {f : α β} {a b : α} (hab : a b) (h : (set.Icc a b)) :
f '' b = set.Icc (has_Inf.Inf (f '' b)) (has_Sup.Sup (f '' b))
theorem continuous_on.image_uIcc_eq_Icc {α : Type u_1} {β : Type u_2} {f : α β} {a b : α} (h : (set.uIcc a b)) :
f '' b = set.Icc (has_Inf.Inf (f '' b)) (has_Sup.Sup (f '' b))
theorem continuous_on.image_uIcc {α : Type u_1} {β : Type u_2} {f : α β} {a b : α} (h : (set.uIcc a b)) :
f '' b = set.uIcc (has_Inf.Inf (f '' b)) (has_Sup.Sup (f '' b))
theorem continuous_on.Inf_image_Icc_le {α : Type u_1} {β : Type u_2} {f : α β} {a b c : α} (h : (set.Icc a b)) (hc : c b) :
has_Inf.Inf (f '' b) f c
theorem continuous_on.le_Sup_image_Icc {α : Type u_1} {β : Type u_2} {f : α β} {a b c : α} (h : (set.Icc a b)) (hc : c b) :
f c has_Sup.Sup (f '' b)
theorem is_compact.exists_local_min_on_mem_subset {α : Type u_1} {β : Type u_2} {f : β α} {s t : set β} {z : β} (ht : is_compact t) (hf : t) (hz : z t) (hfz : (z' : β), z' t \ s f z < f z') :
(x : β) (H : x s), x
theorem is_compact.exists_local_min_mem_open {α : Type u_1} {β : Type u_2} {f : β α} {s t : set β} {z : β} (ht : is_compact t) (hst : s t) (hf : t) (hz : z t) (hfz : (z' : β), z' t \ s f z < f z') (hs : is_open s) :
(x : β) (H : x s), x