Documentation

Mathlib.Topology.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 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) [TopologicalSpace α] [Preorder α] :

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} :
    ∀ {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : CompactIccSpace α] {a b : α}, IsCompact (Set.Icc a b)

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

    theorem CompactIccSpace.mk' {α : Type u_1} [TopologicalSpace α] [Preorder α] (h : ∀ {a b : α}, a bIsCompact (Set.Icc a b)) :
    theorem CompactIccSpace.mk'' {α : Type u_1} [TopologicalSpace α] [PartialOrder α] (h : ∀ {a b : α}, a < bIsCompact (Set.Icc a b)) :
    @[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} [Preorder β] [TopologicalSpace β] [CompactIccSpace β] :
    CompactIccSpace (αβ)
    Equations
    • =
    Equations
    • =
    theorem isCompact_uIcc {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [CompactIccSpace α] {a : α} {b : α} :

    An unordered closed interval is compact.

    @[instance 100]

    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} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] (a : α) (b : α) :
    Equations
    • =

    Extreme value theorem #

    theorem IsCompact.exists_isLeast {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    ∃ (x : α), IsLeast s x
    theorem IsCompact.exists_isGreatest {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    ∃ (x : α), IsGreatest s x
    theorem IsCompact.exists_isGLB {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    xs, IsGLB s x
    theorem IsCompact.exists_isLUB {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    xs, IsLUB s x
    theorem cocompact_le_atBot_atTop {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [CompactIccSpace α] :
    Filter.cocompact α Filter.atBot Filter.atTop
    theorem atBot_atTop_le_cocompact {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMinOrder α] [NoMaxOrder α] [OrderClosedTopology α] :
    Filter.atBot Filter.atTop Filter.cocompact α
    @[simp]
    theorem cocompact_eq_atBot_atTop {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMaxOrder α] [NoMinOrder α] [OrderClosedTopology α] [CompactIccSpace α] :
    Filter.cocompact α = Filter.atBot Filter.atTop
    @[simp]
    @[simp]
    theorem IsCompact.exists_isMinOn {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : βα} (hf : ContinuousOn f s) :
    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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [NoMaxOrder α] {f : βα} {s : Set β} (hs : IsCompact s) (hf : ContinuousOn f s) {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.

    theorem IsCompact.exists_isMaxOn {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : βα} (hf : ContinuousOn f s) :
    xs, IsMaxOn f s 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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} {f : βα} (hf : ContinuousOn f s) (hsc : IsClosed s) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in Filter.cocompact β Filter.principal s, 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.

    theorem ContinuousOn.exists_isMaxOn' {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] {s : Set β} {f : βα} (hf : ContinuousOn f s) (hsc : IsClosed s) {x₀ : β} (h₀ : x₀ s) (hc : ∀ᶠ (x : β) in Filter.cocompact β Filter.principal s, 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.

    theorem Continuous.exists_forall_le' {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {f : βα} (hf : Continuous f) (x₀ : β) (h : ∀ᶠ (x : β) in Filter.cocompact β, 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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] {f : βα} (hf : Continuous f) (x₀ : β) (h : ∀ᶠ (x : β) in Filter.cocompact β, 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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Nonempty β] {f : βα} (hf : Continuous f) (hlim : Filter.Tendsto f (Filter.cocompact β) 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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] [Nonempty β] {f : βα} (hf : Continuous f) (hlim : Filter.Tendsto f (Filter.cocompact β) 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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Nonempty β] [Zero α] {f : βα} (hf : Continuous f) (h : HasCompactSupport f) :
    ∃ (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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] [Nonempty β] [One α] {f : βα} (hf : Continuous f) (h : HasCompactMulSupport f) :
    ∃ (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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] [Nonempty β] [Zero α] {f : βα} (hf : Continuous f) (h : HasCompactSupport f) :
    ∃ (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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] [Nonempty β] [One α] {f : βα} (hf : Continuous f) (h : HasCompactMulSupport f) :
    ∃ (x : β), ∀ (y : β), f y f x

    A continuous function with compact support has a global maximum.

    theorem IsCompact.bddBelow {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] [Nonempty α] {s : Set α} (hs : IsCompact s) :

    A compact set is bounded below

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

    A compact set is bounded above

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

    A continuous function is bounded below on a compact set.

    theorem IsCompact.bddAbove_image {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] [Nonempty α] {f : βα} {K : Set β} (hK : IsCompact K) (hf : ContinuousOn f K) :
    BddAbove (f '' K)

    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.

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

    Min and max elements of a compact set #

    theorem IsCompact.sInf_mem {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    sInf s s
    theorem IsCompact.sSup_mem {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    sSup s s
    theorem IsCompact.isGLB_sInf {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    IsGLB s (sInf s)
    theorem IsCompact.isLUB_sSup {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    IsLUB s (sSup s)
    theorem IsCompact.isLeast_sInf {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    theorem IsCompact.isGreatest_sSup {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) :
    theorem IsCompact.exists_sInf_image_eq_and_le {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : βα} (hf : ContinuousOn f s) :
    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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : βα} (hf : ContinuousOn f s) :
    xs, sSup (f '' s) = f x ys, f y f x
    theorem IsCompact.exists_sInf_image_eq {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : βα} (hf : ContinuousOn f s) :
    xs, sInf (f '' s) = f x
    theorem IsCompact.exists_sSup_image_eq {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : βα} :
    ContinuousOn f sxs, sSup (f '' s) = f x
    theorem IsCompact.exists_isMinOn_mem_subset {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : IsCompact t) (hf : ContinuousOn f t) (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} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : IsCompact t) (hf : ContinuousOn f t) (hz : z t) (hfz : z't \ s, f z' < f z) :
    xs, IsMaxOn f t x
    theorem IsCompact.exists_isLocalMin_mem_open {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIicTopology α] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : IsCompact t) (hst : s t) (hf : ContinuousOn f t) (hz : z t) (hfz : z't \ s, f z < f z') (hs : IsOpen s) :
    xs, IsLocalMin f x
    theorem IsCompact.exists_isLocalMax_mem_open {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [TopologicalSpace β] [ClosedIciTopology α] {f : βα} {s : Set β} {t : Set β} {z : β} (ht : IsCompact t) (hst : s t) (hf : ContinuousOn f t) (hz : z t) (hfz : z't \ s, f z' < f z) (hs : IsOpen s) :
    xs, IsLocalMax f x
    theorem IsCompact.continuous_sSup {α : Type u_2} {β : Type u_3} {γ : Type u_4} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [TopologicalSpace γ] {f : γβα} {K : Set β} (hK : IsCompact K) (hf : Continuous f) :
    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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [TopologicalSpace γ] {f : γβα} {K : Set β} (hK : IsCompact K) (hf : Continuous f) :
    Continuous fun (x : γ) => sInf (f x '' K)

    Image of a closed interval #

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