mathlib documentation

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 also 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 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) [topological_space α] [preorder α] :

Prop

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

@[protected, instance]

def conditionally_complete_linear_order.to_compact_Icc_space (α : Type u_1) [conditionally_complete_linear_order α] [topological_space α] [order_topology α] :

compact_Icc_space α

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_interval {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {a b : α} :

is_compact [a, b]

An unordered closed interval in a conditionally complete linear order is compact.

@[protected, instance]

def compact_space_of_complete_linear_order {α : Type u_1} [complete_linear_order α] [topological_space α] [order_topology α] :

compact_space α

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)

Min and max elements of a compact set #

theorem is_compact.Inf_mem {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

theorem is_compact.Sup_mem {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

theorem is_compact.is_glb_Inf {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

is_glb s (Inf s)

theorem is_compact.is_lub_Sup {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

is_lub s (Sup s)

theorem is_compact.is_least_Inf {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

is_least s (Inf s)

theorem is_compact.is_greatest_Sup {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

is_greatest s (Sup s)

theorem is_compact.exists_is_least {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

∃ (x : α), is_least s x

theorem is_compact.exists_is_greatest {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

∃ (x : α) (H : x ∈ s), is_glb s x

theorem is_compact.exists_is_lub {α : Type u_1} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_compact s) (ne_s : s.nonempty) :

∃ (x : α) (H : x ∈ s), is_lub s x

theorem is_compact.exists_Inf_image_eq {α : Type u_1} {β : Type u_2} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [topological_space β] {s : set β} (hs : is_compact s) (ne_s : s.nonempty) {f : β → α} (hf : continuous_on f s) :

∃ (x : β) (H : x ∈ s), Inf (f '' s) = f x

theorem is_compact.exists_Sup_image_eq {α : Type u_1} {β : Type u_2} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [topological_space β] {s : set β} :

is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s → (∃ (x : β) (H : x ∈ s), 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 (Inf s) (Sup s)

Extreme value theorem #

theorem is_compact.exists_forall_le {α : Type u_1} {β : Type u_2} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [topological_space β] {s : set β} (hs : is_compact s) (ne_s : s.nonempty) {f : β → α} (hf : continuous_on f 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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [topological_space β] {s : set β} :

is_compact s → s.nonempty → ∀ {f : β → α}, continuous_on f s → (∃ (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.exists_forall_le {α : Type u_1} {β : Type u_2} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [topological_space β] [nonempty β] {f : β → α} (hf : continuous f) (hlim : filter.tendsto f (filter.cocompact β) 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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [topological_space β] [nonempty β] {f : β → α} (hf : continuous f) (hlim : filter.tendsto f (filter.cocompact β) 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.

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 (Inf (f '' set.Icc a b)) (Sup (f '' set.Icc a b))

theorem continuous_on.image_interval_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 [a, b]) :

f '' [a, b] = set.Icc (Inf (f '' [a, b])) (Sup (f '' [a, b]))

theorem continuous_on.image_interval {α : 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 [a, b]) :

f '' [a, b] = [Inf (f '' [a, b]), Sup (f '' [a, b])]