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]
- is_compact_Icc : ∀ {a b : α}, is_compact (set.Icc a 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 of this typeclass
@[protected, instance]
def
conditionally_complete_linear_order.to_compact_Icc_space
(α : Type u_1)
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α] :
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 β]
[topological_space β]
[compact_Icc_space β] :
compact_Icc_space (α → β)
@[protected, instance]
def
prod.compact_Icc_space
{α : Type u_1}
{β : Type u_2}
[preorder α]
[topological_space α]
[compact_Icc_space α]
[preorder β]
[topological_space β]
[compact_Icc_space β] :
compact_Icc_space (α × β)
theorem
is_compact_uIcc
{α : Type u_1}
[linear_order α]
[topological_space α]
[compact_Icc_space α]
{a b : α} :
is_compact (set.uIcc a b)
An unordered closed interval is compact.
@[protected, instance]
def
compact_space_of_complete_linear_order
{α : Type u_1}
[complete_linear_order α]
[topological_space α]
[order_topology α] :
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 α]
[topological_space α]
[compact_Icc_space α]
(a b : α) :
compact_space ↥(set.Icc a b)
Extreme value theorem #
theorem
is_compact.exists_is_least
{α : Type u_1}
[linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
theorem
is_compact.exists_is_greatest
{α : Type u_1}
[linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
∃ (x : α), is_greatest s x
theorem
is_compact.exists_is_glb
{α : Type u_1}
[linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
theorem
is_compact.exists_is_lub
{α : Type u_1}
[linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
theorem
is_compact.exists_forall_le
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{s : set β}
(hs : is_compact s)
(ne_s : s.nonempty)
{f : β → α}
(hf : continuous_on f s) :
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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{s : set β} :
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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{s : set β}
{f : β → α}
(hf : continuous_on f s)
(hsc : is_closed s)
{x₀ : β}
(h₀ : x₀ ∈ s)
(hc : ∀ᶠ (x : β) in filter.cocompact β ⊓ filter.principal s, f x₀ ≤ f 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.
theorem
continuous_on.exists_forall_ge'
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{s : set β}
{f : β → α}
(hf : continuous_on f s)
(hsc : is_closed s)
{x₀ : β}
(h₀ : x₀ ∈ s)
(hc : ∀ᶠ (x : β) in filter.cocompact β ⊓ filter.principal s, f x ≤ 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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{f : β → α}
(hf : continuous f)
(x₀ : β)
(h : ∀ᶠ (x : β) in filter.cocompact β, f x₀ ≤ f x) :
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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{f : β → α}
(hf : continuous f)
(x₀ : β)
(h : ∀ᶠ (x : β) in filter.cocompact β, f x ≤ 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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[nonempty β]
{f : β → α}
(hf : continuous f)
(hlim : filter.tendsto f (filter.cocompact β) filter.at_top) :
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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[nonempty β]
{f : β → α}
(hf : continuous f)
(hlim : filter.tendsto f (filter.cocompact β) filter.at_bot) :
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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[nonempty β]
[has_zero α]
{f : β → α}
(hf : continuous f)
(h : has_compact_support f) :
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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[nonempty β]
[has_one α]
{f : β → α}
(hf : continuous f)
(h : has_compact_mul_support f) :
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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[nonempty β]
[has_one α]
{f : β → α}
(hf : continuous f)
(h : has_compact_mul_support f) :
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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[nonempty β]
[has_zero α]
{f : β → α}
(hf : continuous f)
(h : has_compact_support f) :
A continuous function with compact support has a global maximum.
theorem
is_compact.bdd_below
{α : Type u_1}
[linear_order α]
[topological_space α]
[order_closed_topology α]
[nonempty α]
{s : set α}
(hs : is_compact s) :
A compact set is bounded below
theorem
is_compact.bdd_above
{α : Type u_1}
[linear_order α]
[topological_space α]
[order_closed_topology α]
[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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[nonempty α]
{f : β → α}
{K : set β}
(hK : is_compact K)
(hf : continuous_on f 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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[nonempty α]
{f : β → α}
{K : set β}
(hK : is_compact K)
(hf : continuous_on f 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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[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 α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
[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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{f : β → α}
{K : set β}
(hK : is_compact K)
(h0K : K.nonempty)
(hf : continuous_on f K)
(y : α) :
theorem
is_compact.lt_Inf_iff_of_continuous
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
{f : β → α}
{K : set β}
(hK : is_compact K)
(h0K : K.nonempty)
(hf : continuous_on f K)
(y : α) :
Min and max elements of a compact set #
theorem
is_compact.Inf_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
has_Inf.Inf s ∈ s
theorem
is_compact.Sup_mem
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
has_Sup.Sup s ∈ s
theorem
is_compact.is_glb_Inf
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
is_glb s (has_Inf.Inf s)
theorem
is_compact.is_lub_Sup
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
is_lub s (has_Sup.Sup s)
theorem
is_compact.is_least_Inf
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
is_least s (has_Inf.Inf s)
theorem
is_compact.is_greatest_Sup
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
{s : set α}
(hs : is_compact s)
(ne_s : s.nonempty) :
is_greatest s (has_Sup.Sup s)
theorem
is_compact.exists_Inf_image_eq_and_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{s : set β}
(hs : is_compact s)
(ne_s : s.nonempty)
{f : β → α}
(hf : continuous_on f s) :
theorem
is_compact.exists_Sup_image_eq_and_ge
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{s : set β}
(hs : is_compact s)
(ne_s : s.nonempty)
{f : β → α}
(hf : continuous_on f s) :
theorem
is_compact.exists_Inf_image_eq
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{s : set β}
(hs : is_compact s)
(ne_s : s.nonempty)
{f : β → α}
(hf : continuous_on f s) :
theorem
is_compact.exists_Sup_image_eq
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_closed_topology α]
[topological_space β]
{s : set β} :
is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s → (∃ (x : β) (H : x ∈ s), has_Sup.Sup (f '' s) = f x)
theorem
eq_Icc_of_connected_compact
{α : Type u_1}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
{s : set α}
(h₁ : is_connected s)
(h₂ : is_compact s) :
s = set.Icc (has_Inf.Inf s) (has_Sup.Sup s)
theorem
is_compact.continuous_Sup
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
[topological_space γ]
{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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
[topological_space γ]
{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}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
[densely_ordered α]
[conditionally_complete_linear_order β]
[order_topology β]
{f : α → β}
{a b : α}
(hab : a ≤ b)
(h : continuous_on f (set.Icc a b)) :
f '' set.Icc a b = set.Icc (has_Inf.Inf (f '' set.Icc a b)) (has_Sup.Sup (f '' set.Icc a b))
theorem
continuous_on.image_uIcc_eq_Icc
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
[densely_ordered α]
[conditionally_complete_linear_order β]
[order_topology β]
{f : α → β}
{a b : α}
(h : continuous_on f (set.uIcc a b)) :
f '' set.uIcc a b = set.Icc (has_Inf.Inf (f '' set.uIcc a b)) (has_Sup.Sup (f '' set.uIcc a b))
theorem
continuous_on.image_uIcc
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
[densely_ordered α]
[conditionally_complete_linear_order β]
[order_topology β]
{f : α → β}
{a b : α}
(h : continuous_on f (set.uIcc a b)) :
f '' set.uIcc a b = set.uIcc (has_Inf.Inf (f '' set.uIcc a b)) (has_Sup.Sup (f '' set.uIcc a b))
theorem
continuous_on.Inf_image_Icc_le
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
[densely_ordered α]
[conditionally_complete_linear_order β]
[order_topology β]
{f : α → β}
{a b c : α}
(h : continuous_on f (set.Icc a b))
(hc : c ∈ set.Icc a b) :
has_Inf.Inf (f '' set.Icc a b) ≤ f c
theorem
continuous_on.le_Sup_image_Icc
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
[densely_ordered α]
[conditionally_complete_linear_order β]
[order_topology β]
{f : α → β}
{a b c : α}
(h : continuous_on f (set.Icc a b))
(hc : c ∈ set.Icc a b) :
f c ≤ has_Sup.Sup (f '' set.Icc a b)
theorem
is_compact.exists_local_min_on_mem_subset
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
{f : β → α}
{s t : set β}
{z : β}
(ht : is_compact t)
(hf : continuous_on f t)
(hz : z ∈ t)
(hfz : ∀ (z' : β), z' ∈ t \ s → f z < f z') :
∃ (x : β) (H : x ∈ s), is_local_min_on f t x
theorem
is_compact.exists_local_min_mem_open
{α : Type u_1}
{β : Type u_2}
[conditionally_complete_linear_order α]
[topological_space α]
[order_topology α]
[topological_space β]
{f : β → α}
{s t : set β}
{z : β}
(ht : is_compact t)
(hst : s ⊆ t)
(hf : continuous_on f t)
(hz : z ∈ t)
(hfz : ∀ (z' : β), z' ∈ t \ s → f z < f z')
(hs : is_open s) :
∃ (x : β) (H : x ∈ s), is_local_min f x