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.
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.
A closed interval
Set.Icc a b
is a compact set for alla
andb
.
Instances
Equations
- ⋯ = ⋯
A closed interval in a conditionally complete linear order is compact.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
An unordered closed interval is compact.
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
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Extreme value theorem #
The extreme value theorem: a continuous function realizes its minimum on a compact set.
If a continuous function lies strictly above a
on a compact set,
it has a lower bound strictly above a
.
The extreme value theorem: a continuous function realizes its maximum on a compact set.
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.
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.
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.
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.
The extreme value theorem: if a continuous function f
tends to infinity away from compact
sets, then it has a global minimum.
The extreme value theorem: if a continuous function f
tends to negative infinity away from
compact sets, then it has a global maximum.
A continuous function with compact support has a global minimum.
A continuous function with compact support has a global minimum.
A continuous function with compact support has a global maximum.
A continuous function with compact support has a global maximum.
A compact set is bounded below
A compact set is bounded above
A continuous function is bounded below on a compact set.
A continuous function is bounded above on a compact set.
A continuous function with compact support is bounded below.
A continuous function with compact support is bounded below.
A continuous function with compact support is bounded above.
A continuous function with compact support is bounded above.
Min and max elements of a compact set #
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.