doc-next-gen

Mathlib.Topology.Order.Compact

Module docstring

{"# 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. ","### Extreme value theorem ","### Min and max elements of a compact set ","### Image of a closed interval "}

CompactIccSpace structure
(α : Type*) [TopologicalSpace α] [Preorder α]
Full source 
/-- 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. -/
class CompactIccSpace (α : Type*) [TopologicalSpace α] [Preorder α] : Prop where
  /-- A closed interval `Set.Icc a b` is a compact set for all `a` and `b`. -/
  isCompact_Icc : ∀ {a b : α}, IsCompact (Icc a b)
Compact Closed Interval Space
Informal description
A typeclass `CompactIccSpace α` indicates that for any two elements `a` and `b` in a preordered topological space `α` with `a ≤ b`, the closed interval `[a, b]` is compact. This property holds for conditionally complete linear orders with the order topology and their products (both finite and infinite).
CompactIccSpace.mk' theorem
[TopologicalSpace α] [Preorder α] (h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)) : CompactIccSpace α
Full source 
lemma CompactIccSpace.mk' [TopologicalSpace α] [Preorder α]
    (h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)) : CompactIccSpace α where
  isCompact_Icc {a b} := by_cases h fun hab => by rw [Icc_eq_empty hab]; exact isCompact_empty
Characterization of Compact Closed Interval Spaces via Compactness of Intervals
Informal description
Let $\alpha$ be a topological space with a preorder. If for every pair of elements $a, b \in \alpha$ with $a \leq b$, the closed interval $[a, b]$ is compact, then $\alpha$ is a `CompactIccSpace`.
CompactIccSpace.mk'' theorem
[TopologicalSpace α] [PartialOrder α] (h : ∀ {a b : α}, a < b → IsCompact (Icc a b)) : CompactIccSpace α
Full source 
lemma CompactIccSpace.mk'' [TopologicalSpace α] [PartialOrder α]
    (h : ∀ {a b : α}, a < b → IsCompact (Icc a b)) : CompactIccSpace α :=
  .mk' fun hab => hab.eq_or_lt.elim (by rintro rfl; simp) h
Compactness of Closed Intervals via Strict Inequality Condition
Informal description
Let $\alpha$ be a topological space with a partial order. If for every pair of elements $a, b \in \alpha$ with $a < b$, the closed interval $[a, b]$ is compact, then $\alpha$ is a `CompactIccSpace`.
instCompactIccSpaceOrderDual instance
[TopologicalSpace α] [Preorder α] [CompactIccSpace α] : CompactIccSpace (αᵒᵈ)
Full source 
instance [TopologicalSpace α] [Preorder α] [CompactIccSpace α] : CompactIccSpace (αᵒᵈ) where
  isCompact_Icc := by
    intro a b
    convert isCompact_Icc (α := α) (a := b) (b := a) using 1
    exact Icc_toDual (α := α)
Compactness of Closed Intervals in Order Duals
Informal description
For any preordered topological space $\alpha$ where all closed intervals $[a, b]$ are compact, the order dual $\alpha^\mathrm{op}$ also has the property that all closed intervals are compact.
ConditionallyCompleteLinearOrder.toCompactIccSpace instance
(α : Type*) [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] : CompactIccSpace α
Full source 
/-- A closed interval in a conditionally complete linear order is compact. -/
instance (priority := 100) ConditionallyCompleteLinearOrder.toCompactIccSpace (α : Type*)
    [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] :
    CompactIccSpace α := by
  refine .mk'' fun {a b} hlt => ?_
  rcases le_or_lt a b with hab | hab
  swap
  · simp [hab]
  refine isCompact_iff_ultrafilter_le_nhds.2 fun f hf => ?_
  contrapose! hf
  rw [le_principal_iff]
  have hpt : ∀ x ∈ Icc a b, {x} ∉ f := fun x hx hxf =>
    hf x hx ((le_pure_iff.2 hxf).trans (pure_le_nhds x))
  set s := { x ∈ Icc a b | Icc a x ∉ f }
  have hsb : b ∈ upperBounds s := fun x hx => hx.1.2
  have sbd : BddAbove s := ⟨b, hsb⟩
  have ha : a ∈ s := by simp [s, hpt, hab]
  rcases hab.eq_or_lt with (rfl | _hlt)
  · exact ha.2
  -- Porting note: the `obtain` below was instead
  -- `set c := Sup s`
  -- `have hsc : IsLUB s c := isLUB_csSup ⟨a, ha⟩ sbd`
  obtain ⟨c, hsc⟩ : ∃ c, IsLUB s c := ⟨sSup s, isLUB_csSup ⟨a, ha⟩ ⟨b, hsb⟩⟩
  have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
  specialize hf c hc
  have hcs : c ∈ s := by
    rcases hc.1.eq_or_lt with (rfl | hlt); · assumption
    refine ⟨hc, fun hcf => hf fun U hU => ?_⟩
    rcases (mem_nhdsLE_iff_exists_Ioc_subset' hlt).1 (mem_nhdsWithin_of_mem_nhds hU)
      with ⟨x, hxc, hxU⟩
    rcases ((hsc.frequently_mem ⟨a, ha⟩).and_eventually (Ioc_mem_nhdsLE hxc)).exists
      with ⟨y, ⟨_hyab, hyf⟩, hy⟩
    refine mem_of_superset (f.diff_mem_iff.2 ⟨hcf, hyf⟩) (Subset.trans ?_ hxU)
    rw [diff_subset_iff]
    exact Subset.trans Icc_subset_Icc_union_Ioc <| union_subset_union Subset.rfl <|
      Ioc_subset_Ioc_left hy.1.le
  rcases hc.2.eq_or_lt with (rfl | hlt)
  · exact hcs.2
  exfalso
  refine hf fun U hU => ?_
  rcases (mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset hlt).1 (mem_nhdsWithin_of_mem_nhds hU)
    with ⟨y, hxy, hyU⟩
  refine mem_of_superset ?_ hyU; clear! U
  have hy : y ∈ Icc a b := ⟨hc.1.trans hxy.1.le, hxy.2⟩
  by_cases hay : Icc a y ∈ f
  · refine mem_of_superset (f.diff_mem_iff.2 ⟨f.diff_mem_iff.2 ⟨hay, hcs.2⟩, hpt y hy⟩) ?_
    rw [diff_subset_iff, union_comm, Ico_union_right hxy.1.le, diff_subset_iff]
    exact Icc_subset_Icc_union_Icc
  · exact ((hsc.1 ⟨hy, hay⟩).not_lt hxy.1).elim
Compactness of Closed Intervals in Conditionally Complete Linear Orders
Informal description
Every conditionally complete linear order $\alpha$ with the order topology is a `CompactIccSpace`, meaning that all closed intervals $[a, b]$ in $\alpha$ are compact.
instCompactIccSpaceForall instance
{ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)] [∀ i, CompactIccSpace (α i)] : CompactIccSpace (∀ i, α i)
Full source 
instance {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] [∀ i, TopologicalSpace (α i)]
    [∀ i, CompactIccSpace (α i)] : CompactIccSpace (∀ i, α i) :=
  ⟨fun {a b} => (pi_univ_Icc a b ▸ isCompact_univ_pi) fun _ => isCompact_Icc⟩
Compactness of Closed Intervals in Product Spaces
Informal description
For any family of preordered topological spaces $\{\alpha_i\}_{i \in \iota}$ where each $\alpha_i$ has the property that all closed intervals $[a, b]$ are compact, the product space $\prod_{i \in \iota} \alpha_i$ also has this property.
Pi.compact_Icc_space' instance
{α β : Type*} [Preorder β] [TopologicalSpace β] [CompactIccSpace β] : CompactIccSpace (α → β)
Full source 
instance Pi.compact_Icc_space' {α β : Type*} [Preorder β] [TopologicalSpace β]
    [CompactIccSpace β] : CompactIccSpace (α → β) :=
  inferInstance
Compactness of Closed Intervals in Function Spaces
Informal description
For any preordered topological space $\beta$ where all closed intervals $[a, b]$ are compact, the function space $\alpha \to \beta$ (with the product topology) also has this property. That is, for any two functions $f, g \in \alpha \to \beta$ with $f \leq g$ pointwise, the closed interval $[f, g]$ is compact in the function space.
instCompactIccSpaceProd instance
{α β : Type*} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] [Preorder β] [TopologicalSpace β] [CompactIccSpace β] : CompactIccSpace (α × β)
Full source 
instance {α β : Type*} [Preorder α] [TopologicalSpace α] [CompactIccSpace α] [Preorder β]
    [TopologicalSpace β] [CompactIccSpace β] : CompactIccSpace (α × β) :=
  ⟨fun {a b} => (Icc_prod_eq a b).symm ▸ isCompact_Icc.prod isCompact_Icc⟩
Compactness of Closed Intervals in Product Spaces
Informal description
For any two preordered topological spaces $\alpha$ and $\beta$ where all closed intervals are compact, the product space $\alpha \times \beta$ also has this property. That is, for any two pairs $(a_1, a_2), (b_1, b_2) \in \alpha \times \beta$ with $a_1 \leq b_1$ and $a_2 \leq b_2$, the closed interval $[(a_1, a_2), (b_1, b_2)]$ is compact in $\alpha \times \beta$.
isCompact_uIcc theorem
{α : Type*} [LinearOrder α] [TopologicalSpace α] [CompactIccSpace α] {a b : α} : IsCompact (uIcc a b)
Full source 
/-- An unordered closed interval is compact. -/
theorem isCompact_uIcc {α : Type*} [LinearOrder α] [TopologicalSpace α] [CompactIccSpace α]
    {a b : α} : IsCompact (uIcc a b) :=
  isCompact_Icc
Compactness of Unordered Closed Interval in Linearly Ordered Space
Informal description
For any two elements $a$ and $b$ in a linearly ordered topological space $\alpha$ where closed intervals are compact (i.e., $\alpha$ is a `CompactIccSpace`), the unordered closed interval $[a \sqcap b, a \sqcup b]$ is compact.
compactSpace_of_completeLinearOrder instance
{α : Type*} [CompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] : CompactSpace α
Full source 
/-- 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. -/
instance (priority := 100) compactSpace_of_completeLinearOrder {α : Type*} [CompleteLinearOrder α]
    [TopologicalSpace α] [OrderTopology α] : CompactSpace α :=
  ⟨by simp only [← Icc_bot_top, isCompact_Icc]⟩
Compactness of Complete Linear Orders with Order Topology
Informal description
Every complete linear order $\alpha$ with the order topology is a compact space.
compactSpace_Icc instance
(a b : α) : CompactSpace (Icc a b)
Full source 
instance compactSpace_Icc (a b : α) : CompactSpace (Icc a b) :=
  isCompact_iff_compactSpace.mp isCompact_Icc
Compactness of Closed Intervals
Informal description
For any two elements $a$ and $b$ in a preordered topological space $\alpha$, the closed interval $[a, b]$ is a compact space when equipped with the subspace topology.
isCompact_Ico_iff theorem
{a b : α} : IsCompact (Set.Ico a b) ↔ b ≤ a
Full source 
/-- `Set.Ico a b` is only compact if it is empty. -/
@[simp]
theorem isCompact_Ico_iff {a b : α} : IsCompactIsCompact (Set.Ico a b) ↔ b ≤ a :=
  ⟨fun h => isClosed_Ico_iff.mp h.isClosed, by simp_all⟩
Compactness Criterion for Left-Closed Right-Open Interval: $[a, b)$ is compact iff $b \leq a$
Informal description
For any two elements $a$ and $b$ in a preordered type $\alpha$ with order topology, the left-closed right-open interval $[a, b)$ is compact if and only if $b \leq a$.
isCompact_Ioc_iff theorem
{a b : α} : IsCompact (Set.Ioc a b) ↔ b ≤ a
Full source 
/-- `Set.Ioc a b` is only compact if it is empty. -/
@[simp]
theorem isCompact_Ioc_iff {a b : α} : IsCompactIsCompact (Set.Ioc a b) ↔ b ≤ a :=
  ⟨fun h => isClosed_Ioc_iff.mp h.isClosed, by simp_all⟩
Compactness Criterion for Left-Open Right-Closed Interval: $(a, b]$ is compact iff $b \leq a$
Informal description
For any two elements $a$ and $b$ in a preordered type $\alpha$ with order topology, the left-open right-closed interval $(a, b]$ is compact if and only if $b \leq a$.
isCompact_Ioo_iff theorem
{a b : α} : IsCompact (Set.Ioo a b) ↔ b ≤ a
Full source 
/-- `Set.Ioo a b` is only compact if it is empty. -/
@[simp]
theorem isCompact_Ioo_iff {a b : α} : IsCompactIsCompact (Set.Ioo a b) ↔ b ≤ a :=
  ⟨fun h => isClosed_Ioo_iff.mp h.isClosed, by simp_all⟩
Compactness Criterion for Open Interval: $(a, b)$ is compact iff $b \leq a$
Informal description
For any two elements $a$ and $b$ in a preordered type $\alpha$ with order topology, the open interval $(a, b)$ is compact if and only if $b \leq a$.
IsCompact.exists_isLeast theorem
[ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x, IsLeast s x
Full source 
theorem IsCompact.exists_isLeast [ClosedIicTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : ∃ x, IsLeast s x := by
  haveI : Nonempty s := ne_s.to_subtype
  suffices (s ∩ ⋂ x ∈ s, Iic x).Nonempty from
    ⟨this.choose, this.choose_spec.1, mem_iInter₂.mp this.choose_spec.2⟩
  rw [biInter_eq_iInter]
  by_contra H
  rw [not_nonempty_iff_eq_empty] at H
  rcases hs.elim_directed_family_closed (fun x : s => Iic ↑x) (fun x => isClosed_Iic) H
      (Monotone.directed_ge fun _ _ h => Iic_subset_Iic.mpr h) with ⟨x, hx⟩
  exact not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩
Existence of Least Element in Nonempty Compact Sets with `ClosedIicTopology`
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any nonempty compact subset $s \subseteq \alpha$, there exists an element $x \in s$ that is the least element of $s$, i.e., $x \leq y$ for all $y \in s$.
IsCompact.exists_isGreatest theorem
[ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x, IsGreatest s x
Full source 
theorem IsCompact.exists_isGreatest [ClosedIciTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : ∃ x, IsGreatest s x :=
  IsCompact.exists_isLeast (α := αᵒᵈ) hs ne_s
Existence of Greatest Element in Nonempty Compact Sets with `ClosedIciTopology`
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. For any nonempty compact subset $s \subseteq \alpha$, there exists an element $x \in s$ that is the greatest element of $s$, i.e., $x \geq y$ for all $y \in s$.
IsCompact.exists_isGLB theorem
[ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x ∈ s, IsGLB s x
Full source 
theorem IsCompact.exists_isGLB [ClosedIicTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : ∃ x ∈ s, IsGLB s x :=
  (hs.exists_isLeast ne_s).imp (fun x (hx : IsLeast s x) => ⟨hx.1, hx.isGLB⟩)
Existence of Greatest Lower Bound in Nonempty Compact Sets with `ClosedIicTopology`
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property. For any nonempty compact subset $s \subseteq \alpha$, there exists an element $x \in s$ that is the greatest lower bound of $s$, i.e., $x$ is a lower bound of $s$ and any other lower bound $y$ of $s$ satisfies $y \leq x$.
IsCompact.exists_isLUB theorem
[ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x ∈ s, IsLUB s x
Full source 
theorem IsCompact.exists_isLUB [ClosedIciTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : ∃ x ∈ s, IsLUB s x :=
  IsCompact.exists_isGLB (α := αᵒᵈ) hs ne_s
Existence of Least Upper Bound in Nonempty Compact Sets with `ClosedIciTopology`
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property. For any nonempty compact subset $s \subseteq \alpha$, there exists an element $x \in s$ that is the least upper bound of $s$, i.e., $x$ is an upper bound of $s$ and any other upper bound $y$ of $s$ satisfies $x \leq y$.
cocompact_le_atBot_atTop theorem
[CompactIccSpace α] : cocompact α ≤ atBot ⊔ atTop
Full source 
theorem cocompact_le_atBot_atTop [CompactIccSpace α] :
    cocompact α ≤ atBotatBot ⊔ atTop := by
  refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro
  · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
  · obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs.1
    obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2
    refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩
    exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_le h)) fun h ↦ hu x (le_of_not_le h)
Cocompact Filter is Finer than Join of `atBot` and `atTop` in `CompactIccSpace`
Informal description
In a topological space $\alpha$ with the `CompactIccSpace` property, the cocompact filter is finer than the join of the filters `atBot` and `atTop`. In other words, every set that is eventually bounded below and above is cocompact.
cocompact_le_atBot theorem
[OrderTop α] [CompactIccSpace α] : cocompact α ≤ atBot
Full source 
theorem cocompact_le_atBot [OrderTop α] [CompactIccSpace α] :
    cocompact α ≤ atBot := by
  refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro
  · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
  · obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
    refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩
    exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_le h)) (fun h ↦ (h le_top).elim)
Cocompact Filter is Finer than `atBot` in `CompactIccSpace` with Top Element
Informal description
In a topological space $\alpha$ with a greatest element and where every closed interval is compact, the cocompact filter is finer than the filter of sets that are eventually bounded below. In other words, every set that is eventually bounded below is cocompact.
cocompact_le_atTop theorem
[OrderBot α] [CompactIccSpace α] : cocompact α ≤ atTop
Full source 
theorem cocompact_le_atTop [OrderBot α] [CompactIccSpace α] :
    cocompact α ≤ atTop :=
  cocompact_le_atBot (α := αᵒᵈ)
Cocompact Filter is Finer than `atTop` in `CompactIccSpace` with Bottom Element
Informal description
In a topological space $\alpha$ with a least element and where every closed interval is compact, the cocompact filter is finer than the filter of sets that are eventually bounded above. In other words, every set that is eventually bounded above is cocompact.
atBot_le_cocompact theorem
[NoMinOrder α] [ClosedIicTopology α] : atBot ≤ cocompact α
Full source 
theorem atBot_le_cocompact [NoMinOrder α] [ClosedIicTopology α] :
    atBot ≤ cocompact α := by
  refine fun s hs ↦ ?_
  obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
  refine (Set.eq_empty_or_nonempty t).casesOn (fun h_empty ↦ ?_) (fun h_nonempty ↦ ?_)
  · rewrite [compl_univ_iff.mpr h_empty, univ_subset_iff] at hts
    convert univ_mem
  · haveI := h_nonempty.nonempty
    obtain ⟨a, ha⟩ := ht.exists_isLeast h_nonempty
    obtain ⟨b, hb⟩ := exists_lt a
    exact Filter.mem_atBot_sets.mpr ⟨b, fun b' hb' ↦ hts <| Classical.byContradiction
      fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_not_mem.mp hc)⟩
Cocompact Sets are Eventually Bounded Below in No-Min-Order Spaces with Closed Lower Intervals
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and assume $\alpha$ has no minimal element. Then the filter of sets that are eventually bounded below is finer than the cocompact filter. In other words, every cocompact set is eventually bounded below.
atTop_le_cocompact theorem
[NoMaxOrder α] [ClosedIciTopology α] : atTop ≤ cocompact α
Full source 
theorem atTop_le_cocompact [NoMaxOrder α] [ClosedIciTopology α] :
    atTop ≤ cocompact α :=
  atBot_le_cocompact (α := αᵒᵈ)
Cocompact Sets are Eventually Bounded Above in No-Max-Order Spaces with Closed Upper Intervals
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property, and assume $\alpha$ has no maximal element. Then the filter of sets that are eventually bounded above is finer than the cocompact filter. In other words, every cocompact set is eventually bounded above.
atBot_atTop_le_cocompact theorem
[NoMinOrder α] [NoMaxOrder α] [OrderClosedTopology α] : atBot ⊔ atTop ≤ cocompact α
Full source 
theorem atBot_atTop_le_cocompact [NoMinOrder α] [NoMaxOrder α]
    [OrderClosedTopology α] : atBotatBot ⊔ atTop ≤ cocompact α :=
  sup_le atBot_le_cocompact atTop_le_cocompact
Cocompact Sets are Eventually Bounded in Both Directions in No-Min-Max-Order Spaces with Order-Closed Topology
Informal description
Let $\alpha$ be a topological space with a preorder, no minimal element, no maximal element, and an order-closed topology. Then the supremum of the filters of sets that are eventually bounded below and eventually bounded above is finer than the cocompact filter. In other words, every cocompact set is eventually bounded both below and above.
cocompact_eq_atBot_atTop theorem
[NoMaxOrder α] [NoMinOrder α] [OrderClosedTopology α] [CompactIccSpace α] : cocompact α = atBot ⊔ atTop
Full source 
@[simp 900]
theorem cocompact_eq_atBot_atTop [NoMaxOrder α] [NoMinOrder α]
    [OrderClosedTopology α] [CompactIccSpace α] : cocompact α = atBotatBot ⊔ atTop :=
  cocompact_le_atBot_atTop.antisymm atBot_atTop_le_cocompact
Cocompact Filter Characterization in No-Min-Max-Order Spaces with Compact Intervals
Informal description
Let $\alpha$ be a topological space equipped with a preorder, no minimal element, no maximal element, an order-closed topology, and where every closed interval is compact. Then the cocompact filter on $\alpha$ coincides with the join of the filters `atBot` and `atTop`. In other words, a set is cocompact if and only if it is eventually bounded both below and above.
cocompact_eq_atBot theorem
[NoMinOrder α] [OrderTop α] [ClosedIicTopology α] [CompactIccSpace α] : cocompact α = atBot
Full source 
@[simp]
theorem cocompact_eq_atBot [NoMinOrder α] [OrderTop α]
    [ClosedIicTopology α] [CompactIccSpace α] : cocompact α = atBot :=
  cocompact_le_atBot.antisymm atBot_le_cocompact
Cocompact Filter Equals `atBot` in No-Min-Order Space with Top Element and Compact Intervals
Informal description
Let $\alpha$ be a topological space with a preorder, no minimal element, and a greatest element $\top$, where every closed interval is compact and all lower intervals $\{x \in \alpha \mid x \leq a\}$ are closed. Then the cocompact filter on $\alpha$ coincides with the filter of sets that are eventually bounded below.
cocompact_eq_atTop theorem
[NoMaxOrder α] [OrderBot α] [ClosedIciTopology α] [CompactIccSpace α] : cocompact α = atTop
Full source 
@[simp]
theorem cocompact_eq_atTop [NoMaxOrder α] [OrderBot α]
    [ClosedIciTopology α] [CompactIccSpace α] : cocompact α = atTop :=
  cocompact_le_atTop.antisymm atTop_le_cocompact
Cocompact Filter Equals `atTop` in No-Max-Order Space with Bottom Element and Compact Intervals
Informal description
Let $\alpha$ be a topological space with a preorder, no maximal elements, and a least element $\bot$, where every closed interval is compact and all upper intervals $\{x \in \alpha \mid x \geq a\}$ are closed. Then the cocompact filter on $\alpha$ coincides with the filter of sets that are eventually bounded above.
IsCompact.exists_isMinOn theorem
[ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, IsMinOn f s x
Full source 
/-- The **extreme value theorem**: a continuous function realizes its minimum on a compact set. -/
theorem IsCompact.exists_isMinOn [ClosedIicTopology α] {s : Set β} (hs : IsCompact s)
    (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, IsMinOn f s x := by
  rcases (hs.image_of_continuousOn hf).exists_isLeast (ne_s.image f) with ⟨_, ⟨x, hxs, rfl⟩, hx⟩
  refine ⟨x, hxs, forall_mem_image.1 (fun _ hb => hx <| mem_image_of_mem f ?_)⟩
  rwa [(image_id' s).symm]
Existence of Minimum for Continuous Functions on Compact Sets (Extreme Value Theorem)
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be another topological space. For any nonempty compact subset $s \subseteq \beta$ and any continuous function $f : \beta \to \alpha$ defined on $s$, there exists an element $x \in s$ such that $f(x) \leq f(y)$ for all $y \in s$.
IsCompact.exists_forall_le' theorem
[ClosedIicTopology α] [NoMaxOrder α] {f : β → α} {s : Set β} (hs : IsCompact s) (hf : ContinuousOn f s) {a : α} (hf' : ∀ b ∈ s, a < f b) : ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b
Full source 
/-- If a continuous function lies strictly above `a` on a compact set,
  it has a lower bound strictly above `a`. -/
theorem IsCompact.exists_forall_le' [ClosedIicTopology α] [NoMaxOrder α] {f : β → α}
    {s : Set β} (hs : IsCompact s) (hf : ContinuousOn f s) {a : α} (hf' : ∀ b ∈ s, a < f b) :
    ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b := by
  rcases s.eq_empty_or_nonempty with (rfl | hs')
  · obtain ⟨a', ha'⟩ := exists_gt a
    exact ⟨a', ha', fun _ a ↦ a.elim⟩
  · obtain ⟨x, hx, hx'⟩ := hs.exists_isMinOn hs' hf
    exact ⟨f x, hf' x hx, hx'⟩
Existence of Lower Bound for Continuous Functions on Compact Sets (Strictly Above Given Value)
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and assume $\alpha$ has no maximal elements. Let $\beta$ be another topological space, $s \subseteq \beta$ a compact subset, and $f : \beta \to \alpha$ a continuous function on $s$. If there exists a real number $a$ such that $a < f(b)$ for all $b \in s$, then there exists $a' \in \alpha$ such that $a < a'$ and $a' \leq f(b)$ for all $b \in s$.
IsCompact.exists_isMaxOn theorem
[ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, IsMaxOn f s x
Full source 
/-- The **extreme value theorem**: a continuous function realizes its maximum on a compact set. -/
theorem IsCompact.exists_isMaxOn [ClosedIciTopology α] {s : Set β} (hs : IsCompact s)
    (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, IsMaxOn f s x :=
  IsCompact.exists_isMinOn (α := αᵒᵈ) hs ne_s hf
Existence of Maximum for Continuous Functions on Compact Sets (Extreme Value Theorem)
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (where all upper intervals $[a, \infty)$ are closed), and let $\beta$ be another topological space. For any nonempty compact subset $s \subseteq \beta$ and any continuous function $f : \beta \to \alpha$ defined on $s$, there exists an element $x \in s$ such that $f(x) \geq f(y)$ for all $y \in s$.
ContinuousOn.exists_isMinOn' theorem
[ClosedIicTopology α] {s : Set β} {f : β → α} (hf : ContinuousOn f s) (hsc : IsClosed s) {x₀ : β} (h₀ : x₀ ∈ s) (hc : ∀ᶠ x in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x) : ∃ x ∈ s, IsMinOn f s x
Full source 
/-- 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_isMinOn' [ClosedIicTopology α] {s : Set β} {f : β → α}
    (hf : ContinuousOn f s) (hsc : IsClosed s) {x₀ : β} (h₀ : x₀ ∈ s)
    (hc : ∀ᶠ x in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x) : ∃ x ∈ s, IsMinOn f s x := by
  rcases (hasBasis_cocompact.inf_principal _).eventually_iff.1 hc with ⟨K, hK, hKf⟩
  have hsub : insertinsert x₀ (K ∩ s) ⊆ s := insert_subset_iff.2 ⟨h₀, inter_subset_right⟩
  obtain ⟨x, hx, hxf⟩ : ∃ x ∈ insert x₀ (K ∩ s), ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y :=
    ((hK.inter_right hsc).insert x₀).exists_isMinOn (insert_nonempty _ _) (hf.mono hsub)
  refine ⟨x, hsub hx, fun y hy => ?_⟩
  by_cases hyK : y ∈ K
  exacts [hxf _ (Or.inr ⟨hyK, hy⟩), (hxf _ (Or.inl rfl)).trans (hKf ⟨hyK, hy⟩)]
Existence of Minimum for Continuous Functions on Closed Sets with Cocompact Condition (Extreme Value Theorem Variant)
Informal description
Let $\alpha$ be a topological space with the `ClosedIicTopology` property, and let $\beta$ be another topological space. Given a closed subset $s \subseteq \beta$, a continuous function $f \colon \beta \to \alpha$ defined on $s$, and a point $x_0 \in s$ such that $f(x_0) \leq f(x)$ for all $x$ in the intersection of $s$ with the cocompact filter of $\beta$, there exists a point $x \in s$ that minimizes $f$ on $s$, i.e., $f(x) \leq f(y)$ for all $y \in s$.
ContinuousOn.exists_isMaxOn' theorem
[ClosedIciTopology α] {s : Set β} {f : β → α} (hf : ContinuousOn f s) (hsc : IsClosed s) {x₀ : β} (h₀ : x₀ ∈ s) (hc : ∀ᶠ x in cocompact β ⊓ 𝓟 s, f x ≤ f x₀) : ∃ x ∈ s, IsMaxOn f s x
Full source 
/-- 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 ContinuousOn.exists_isMaxOn' [ClosedIciTopology α] {s : Set β} {f : β → α}
    (hf : ContinuousOn f s) (hsc : IsClosed s) {x₀ : β} (h₀ : x₀ ∈ s)
    (hc : ∀ᶠ x in cocompact β ⊓ 𝓟 s, f x ≤ f x₀) : ∃ x ∈ s, IsMaxOn f s x :=
  ContinuousOn.exists_isMinOn' (α := αᵒᵈ) hf hsc h₀ hc
Existence of Maximum for Continuous Functions on Closed Sets with Cocompact Condition (Extreme Value Theorem Variant)
Informal description
Let $\alpha$ be a topological space with the `ClosedIciTopology` property (where all upper intervals $[a, \infty)$ are closed), and let $\beta$ be another topological space. Given a closed subset $s \subseteq \beta$, a continuous function $f \colon \beta \to \alpha$ defined on $s$, and a point $x_0 \in s$ such that $f(x) \leq f(x_0)$ for all $x$ in the intersection of $s$ with the cocompact filter of $\beta$, there exists a point $x \in s$ that maximizes $f$ on $s$, i.e., $f(y) \leq f(x)$ for all $y \in s$.
Continuous.exists_forall_le' theorem
[ClosedIicTopology α] {f : β → α} (hf : Continuous f) (x₀ : β) (h : ∀ᶠ x in cocompact β, f x₀ ≤ f x) : ∃ x : β, ∀ y : β, f x ≤ f y
Full source 
/-- 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_le' [ClosedIicTopology α] {f : β → α} (hf : Continuous f)
    (x₀ : β) (h : ∀ᶠ x in cocompact β, f x₀ ≤ f x) : ∃ x : β, ∀ y : β, f x ≤ f y :=
  let ⟨x, _, hx⟩ := hf.continuousOn.exists_isMinOn' isClosed_univ (mem_univ x₀)
    (by rwa [principal_univ, inf_top_eq])
  ⟨x, fun y => hx (mem_univ y)⟩
Existence of Global Minimum for Continuous Functions (Extreme Value Theorem)
Informal description
Let $\alpha$ be a topological space with the `ClosedIicTopology` property, and let $f \colon \beta \to \alpha$ be a continuous function. If there exists a point $x_0 \in \beta$ such that $f(x_0) \leq f(x)$ for all $x$ in the cocompact filter of $\beta$, then there exists a global minimum point $x \in \beta$ for $f$, i.e., $f(x) \leq f(y)$ for all $y \in \beta$.
Continuous.exists_forall_ge' theorem
[ClosedIciTopology α] {f : β → α} (hf : Continuous f) (x₀ : β) (h : ∀ᶠ x in cocompact β, f x ≤ f x₀) : ∃ x : β, ∀ y : β, f y ≤ f x
Full source 
/-- 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_ge' [ClosedIciTopology α] {f : β → α} (hf : Continuous f)
    (x₀ : β) (h : ∀ᶠ x in cocompact β, f x ≤ f x₀) : ∃ x : β, ∀ y : β, f y ≤ f x :=
  Continuous.exists_forall_le' (α := αᵒᵈ) hf x₀ h
Existence of Global Maximum for Continuous Functions (Extreme Value Theorem)
Informal description
Let $\alpha$ be a topological space with the `ClosedIciTopology` property (where all upper intervals $[a, \infty)$ are closed), and let $f \colon \beta \to \alpha$ be a continuous function. If there exists a point $x_0 \in \beta$ such that $f(x) \leq f(x_0)$ for all $x$ in the cocompact filter of $\beta$, then there exists a global maximum point $x \in \beta$ for $f$, i.e., $f(y) \leq f(x)$ for all $y \in \beta$.
Continuous.exists_forall_le theorem
[ClosedIicTopology α] [Nonempty β] {f : β → α} (hf : Continuous f) (hlim : Tendsto f (cocompact β) atTop) : ∃ x, ∀ y, f x ≤ f y
Full source 
/-- 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_le [ClosedIicTopology α] [Nonempty β] {f : β → α}
    (hf : Continuous f) (hlim : Tendsto f (cocompact β) atTop) : ∃ x, ∀ y, f x ≤ f y := by
  inhabit β
  exact hf.exists_forall_le' default (hlim.eventually <| eventually_ge_atTop _)
Extreme Value Theorem: Existence of Global Minimum for Continuous Functions Tending to Infinity
Informal description
Let $\alpha$ be a topological space with the `ClosedIicTopology` property, and let $\beta$ be a nonempty topological space. If $f \colon \beta \to \alpha$ is a continuous function such that $f$ tends to infinity along the cocompact filter of $\beta$, then there exists a point $x \in \beta$ such that $f(x) \leq f(y)$ for all $y \in \beta$.
Continuous.exists_forall_ge theorem
[ClosedIciTopology α] [Nonempty β] {f : β → α} (hf : Continuous f) (hlim : Tendsto f (cocompact β) atBot) : ∃ x, ∀ y, f y ≤ f x
Full source 
/-- 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_ge [ClosedIciTopology α] [Nonempty β] {f : β → α}
    (hf : Continuous f) (hlim : Tendsto f (cocompact β) atBot) : ∃ x, ∀ y, f y ≤ f x :=
  Continuous.exists_forall_le (α := αᵒᵈ) hf hlim
Extreme Value Theorem: Existence of Global Maximum for Continuous Functions Tending to Negative Infinity
Informal description
Let $\alpha$ be a topological space with the `ClosedIciTopology` property (where all upper intervals $[a, \infty)$ are closed), and let $\beta$ be a nonempty topological space. If $f \colon \beta \to \alpha$ is a continuous function such that $f$ tends to negative infinity along the cocompact filter of $\beta$, then there exists a point $x \in \beta$ such that $f(y) \leq f(x)$ for all $y \in \beta$.
Continuous.exists_forall_le_of_hasCompactMulSupport theorem
[ClosedIicTopology α] [Nonempty β] [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) : ∃ x : β, ∀ y : β, f x ≤ f y
Full source 
/-- A continuous function with compact support has a global minimum. -/
@[to_additive "A continuous function with compact support has a global minimum."]
theorem Continuous.exists_forall_le_of_hasCompactMulSupport [ClosedIicTopology α] [Nonempty β]
    [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) :
    ∃ x : β, ∀ y : β, f x ≤ f y := by
  obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.isCompact_range hf).exists_isLeast (range_nonempty _)
  rw [mem_lowerBounds, forall_mem_range] at hx
  exact ⟨x, hx⟩
Existence of Global Minimum for Continuous Functions with Compact Multiplicative Support
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be a nonempty type with a distinguished element $1 \in \alpha$. Given a continuous function $f \colon \beta \to \alpha$ with compact multiplicative support, there exists a point $x \in \beta$ such that $f(x) \leq f(y)$ for all $y \in \beta$.
Continuous.exists_forall_ge_of_hasCompactMulSupport theorem
[ClosedIciTopology α] [Nonempty β] [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) : ∃ x : β, ∀ y : β, f y ≤ f x
Full source 
/-- A continuous function with compact support has a global maximum. -/
@[to_additive "A continuous function with compact support has a global maximum."]
theorem Continuous.exists_forall_ge_of_hasCompactMulSupport [ClosedIciTopology α] [Nonempty β]
    [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) :
    ∃ x : β, ∀ y : β, f y ≤ f x :=
  Continuous.exists_forall_le_of_hasCompactMulSupport (α := αᵒᵈ) hf h
Existence of Global Maximum for Continuous Functions with Compact Multiplicative Support
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed), and let $\beta$ be a nonempty type with a distinguished element $1 \in \alpha$. Given a continuous function $f \colon \beta \to \alpha$ with compact multiplicative support, there exists a point $x \in \beta$ such that $f(y) \leq f(x)$ for all $y \in \beta$.
IsCompact.bddBelow theorem
[ClosedIicTopology α] [Nonempty α] {s : Set α} (hs : IsCompact s) : BddBelow s
Full source 
/-- A compact set is bounded below -/
theorem IsCompact.bddBelow [ClosedIicTopology α] [Nonempty α] {s : Set α} (hs : IsCompact s) :
    BddBelow s := by
  rcases s.eq_empty_or_nonempty with rfl | hne
  · exact bddBelow_empty
  · obtain ⟨a, -, has⟩ := hs.exists_isLeast hne
    exact ⟨a, has⟩
Compact sets are bounded below in `ClosedIicTopology` spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed). If $s$ is a nonempty compact subset of $\alpha$, then $s$ is bounded below.
IsCompact.bddAbove theorem
[ClosedIciTopology α] [Nonempty α] {s : Set α} (hs : IsCompact s) : BddAbove s
Full source 
/-- A compact set is bounded above -/
theorem IsCompact.bddAbove [ClosedIciTopology α] [Nonempty α] {s : Set α} (hs : IsCompact s) :
    BddAbove s :=
  IsCompact.bddBelow (α := αᵒᵈ) hs
Compact sets are bounded above in `ClosedIciTopology` spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed). If $s$ is a nonempty compact subset of $\alpha$, then $s$ is bounded above.
IsCompact.bddBelow_image theorem
[ClosedIicTopology α] [Nonempty α] {f : β → α} {K : Set β} (hK : IsCompact K) (hf : ContinuousOn f K) : BddBelow (f '' K)
Full source 
/-- A continuous function is bounded below on a compact set. -/
theorem IsCompact.bddBelow_image [ClosedIicTopology α] [Nonempty α] {f : β → α} {K : Set β}
    (hK : IsCompact K) (hf : ContinuousOn f K) : BddBelow (f '' K) :=
  (hK.image_of_continuousOn hf).bddBelow
Continuous Image of Compact Set is Bounded Below in `ClosedIicTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed). Let $K$ be a nonempty compact subset of a topological space $\beta$, and $f : \beta \to \alpha$ a function that is continuous on $K$. Then the image $f(K)$ is bounded below in $\alpha$.
IsCompact.bddAbove_image theorem
[ClosedIciTopology α] [Nonempty α] {f : β → α} {K : Set β} (hK : IsCompact K) (hf : ContinuousOn f K) : BddAbove (f '' K)
Full source 
/-- A continuous function is bounded above on a compact set. -/
theorem IsCompact.bddAbove_image [ClosedIciTopology α] [Nonempty α] {f : β → α} {K : Set β}
    (hK : IsCompact K) (hf : ContinuousOn f K) : BddAbove (f '' K) :=
  IsCompact.bddBelow_image (α := αᵒᵈ) hK hf
Continuous Image of Compact Set is Bounded Above in `ClosedIciTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed). Let $K$ be a nonempty compact subset of a topological space $\beta$, and $f : \beta \to \alpha$ a continuous function on $K$. Then the image $f(K)$ is bounded above in $\alpha$.
Continuous.bddBelow_range_of_hasCompactMulSupport theorem
[ClosedIicTopology α] [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) : BddBelow (range f)
Full source 
/-- A continuous function with compact support is bounded below. -/
@[to_additive "A continuous function with compact support is bounded below."]
theorem Continuous.bddBelow_range_of_hasCompactMulSupport [ClosedIicTopology α] [One α]
    {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) : BddBelow (range f) :=
  (h.isCompact_range hf).bddBelow
Continuous functions with compact multiplicative support have bounded below range
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed), and let $\alpha$ have a distinguished element $1$. Let $f : \beta \to \alpha$ be a continuous function with compact multiplicative support. Then the range of $f$ is bounded below in $\alpha$.
Continuous.bddAbove_range_of_hasCompactMulSupport theorem
[ClosedIciTopology α] [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) : BddAbove (range f)
Full source 
/-- A continuous function with compact support is bounded above. -/
@[to_additive "A continuous function with compact support is bounded above."]
theorem Continuous.bddAbove_range_of_hasCompactMulSupport [ClosedIciTopology α] [One α]
    {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) : BddAbove (range f) :=
  Continuous.bddBelow_range_of_hasCompactMulSupport (α := αᵒᵈ) hf h
Continuous functions with compact multiplicative support have bounded above range
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed), and let $\alpha$ have a distinguished element $1$. If $f : \beta \to \alpha$ is a continuous function with compact multiplicative support, then the range of $f$ is bounded above in $\alpha$.
IsCompact.sSup_lt_iff_of_continuous theorem
[ClosedIciTopology α] {f : β → α} {K : Set β} (hK : IsCompact K) (h0K : K.Nonempty) (hf : ContinuousOn f K) (y : α) : sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y
Full source 
theorem IsCompact.sSup_lt_iff_of_continuous [ClosedIciTopology α] {f : β → α} {K : Set β}
    (hK : IsCompact K) (h0K : K.Nonempty) (hf : ContinuousOn f K) (y : α) :
    sSupsSup (f '' K) < y ↔ ∀ x ∈ K, f x < y := by
  refine ⟨fun h x hx => (le_csSup (hK.bddAbove_image hf) <| mem_image_of_mem f hx).trans_lt h,
    fun h => ?_⟩
  obtain ⟨x, hx, h2x⟩ := hK.exists_isMaxOn h0K hf
  refine (csSup_le (h0K.image f) ?_).trans_lt (h x hx)
  rintro _ ⟨x', hx', rfl⟩; exact h2x hx'
Supremum of Continuous Image is Less Than $y$ if and only if All Values Are Less Than $y$
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed). Let $K$ be a nonempty compact subset of a topological space $\beta$, and $f : \beta \to \alpha$ a continuous function on $K$. For any $y \in \alpha$, the supremum of the image $f(K)$ is strictly less than $y$ if and only if $f(x) < y$ for all $x \in K$.
IsCompact.lt_sInf_iff_of_continuous theorem
[ClosedIicTopology α] {f : β → α} {K : Set β} (hK : IsCompact K) (h0K : K.Nonempty) (hf : ContinuousOn f K) (y : α) : y < sInf (f '' K) ↔ ∀ x ∈ K, y < f x
Full source 
theorem IsCompact.lt_sInf_iff_of_continuous [ClosedIicTopology α] {f : β → α} {K : Set β}
    (hK : IsCompact K) (h0K : K.Nonempty) (hf : ContinuousOn f K) (y : α) :
    y < sInf (f '' K) ↔ ∀ x ∈ K, y < f x :=
  IsCompact.sSup_lt_iff_of_continuous (α := αᵒᵈ) hK h0K hf y
Infimum of Continuous Image is Greater Than $y$ if and only if All Values Are Greater Than $y$
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed). Let $K$ be a nonempty compact subset of a topological space $\beta$, and $f : \beta \to \alpha$ a continuous function on $K$. For any $y \in \alpha$, we have $y < \inf f(K)$ if and only if $y < f(x)$ for all $x \in K$.
IsCompact.sInf_mem theorem
[ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : sInf s ∈ s
Full source 
theorem IsCompact.sInf_mem [ClosedIicTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : sInfsInf s ∈ s :=
  let ⟨_a, ha⟩ := hs.exists_isLeast ne_s
  ha.csInf_mem
Infimum of Nonempty Compact Set Belongs to the Set in `ClosedIicTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed). For any nonempty compact subset $s \subseteq \alpha$, the infimum of $s$ is an element of $s$.
IsCompact.sSup_mem theorem
[ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : sSup s ∈ s
Full source 
theorem IsCompact.sSup_mem [ClosedIciTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : sSupsSup s ∈ s :=
  IsCompact.sInf_mem (α := αᵒᵈ) hs ne_s
Supremum of Nonempty Compact Set Belongs to the Set in `ClosedIciTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed). For any nonempty compact subset $s \subseteq \alpha$, the supremum of $s$ is an element of $s$.
IsCompact.isGLB_sInf theorem
[ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsGLB s (sInf s)
Full source 
theorem IsCompact.isGLB_sInf [ClosedIicTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : IsGLB s (sInf s) :=
  isGLB_csInf ne_s hs.bddBelow
Infimum is Greatest Lower Bound for Nonempty Compact Sets in `ClosedIicTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed). For any nonempty compact subset $s \subseteq \alpha$, the infimum $\inf s$ is the greatest lower bound of $s$. That is: 1. $\inf s$ is a lower bound of $s$ (i.e., $\inf s \leq x$ for all $x \in s$), and 2. for any other lower bound $l$ of $s$, we have $l \leq \inf s$.
IsCompact.isLUB_sSup theorem
[ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsLUB s (sSup s)
Full source 
theorem IsCompact.isLUB_sSup [ClosedIciTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : IsLUB s (sSup s) :=
  IsCompact.isGLB_sInf (α := αᵒᵈ) hs ne_s
Supremum is Least Upper Bound for Nonempty Compact Sets in `ClosedIciTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed). For any nonempty compact subset $s \subseteq \alpha$, the supremum $\sup s$ is the least upper bound of $s$. That is: 1. $\sup s$ is an upper bound of $s$ (i.e., $x \leq \sup s$ for all $x \in s$), and 2. for any other upper bound $u$ of $s$, we have $\sup s \leq u$.
IsCompact.isLeast_sInf theorem
[ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsLeast s (sInf s)
Full source 
theorem IsCompact.isLeast_sInf [ClosedIicTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : IsLeast s (sInf s) :=
  ⟨hs.sInf_mem ne_s, (hs.isGLB_sInf ne_s).1⟩
Infimum is Least Element in Nonempty Compact Sets with Closed Lower Intervals
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed). For any nonempty compact subset $s \subseteq \alpha$, the infimum $\inf s$ is the least element of $s$. That is: 1. $\inf s \in s$, and 2. $\inf s \leq x$ for all $x \in s$.
IsCompact.isGreatest_sSup theorem
[ClosedIciTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : IsGreatest s (sSup s)
Full source 
theorem IsCompact.isGreatest_sSup [ClosedIciTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : IsGreatest s (sSup s) :=
  IsCompact.isLeast_sInf (α := αᵒᵈ) hs ne_s
Supremum is Greatest Element in Nonempty Compact Sets with Closed Upper Intervals
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed). For any nonempty compact subset $s \subseteq \alpha$, the supremum $\sup s$ is the greatest element of $s$. That is: 1. $\sup s \in s$, and 2. $x \leq \sup s$ for all $x \in s$.
IsCompact.exists_sInf_image_eq_and_le theorem
[ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, sInf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y
Full source 
theorem IsCompact.exists_sInf_image_eq_and_le [ClosedIicTopology α] {s : Set β}
    (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) :
    ∃ x ∈ s, sInf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y :=
  let ⟨x, hxs, hx⟩ := (hs.image_of_continuousOn hf).sInf_mem (ne_s.image f)
  ⟨x, hxs, hx.symm, fun _y hy =>
    hx.trans_le <| csInf_le (hs.image_of_continuousOn hf).bddBelow <| mem_image_of_mem f hy⟩
Existence of Minimizer for Continuous Function on Compact Set in `ClosedIicTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed). Let $s$ be a nonempty compact subset of a topological space $\beta$, and $f : \beta \to \alpha$ a function continuous on $s$. Then there exists a point $x \in s$ such that: 1. The infimum of $f$ over $s$ is achieved at $x$, i.e., $\inf f(s) = f(x)$. 2. For all $y \in s$, we have $f(x) \leq f(y)$.
IsCompact.exists_sSup_image_eq_and_ge theorem
[ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, sSup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x
Full source 
theorem IsCompact.exists_sSup_image_eq_and_ge [ClosedIciTopology α] {s : Set β}
    (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) :
    ∃ x ∈ s, sSup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x :=
  IsCompact.exists_sInf_image_eq_and_le (α := αᵒᵈ) hs ne_s hf
Existence of Maximizer for Continuous Function on Compact Set in `ClosedIciTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIciTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \geq a\}$ is closed). Let $s$ be a nonempty compact subset of a topological space $\beta$, and $f : \beta \to \alpha$ a function continuous on $s$. Then there exists a point $x \in s$ such that: 1. The supremum of $f$ over $s$ is achieved at $x$, i.e., $\sup f(s) = f(x)$. 2. For all $y \in s$, we have $f(y) \leq f(x)$.
IsCompact.exists_sInf_image_eq theorem
[ClosedIicTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, sInf (f '' s) = f x
Full source 
theorem IsCompact.exists_sInf_image_eq [ClosedIicTopology α] {s : Set β} (hs : IsCompact s)
    (ne_s : s.Nonempty) {f : β → α} (hf : ContinuousOn f s) : ∃ x ∈ s, sInf (f '' s) = f x :=
  let ⟨x, hxs, hx, _⟩ := hs.exists_sInf_image_eq_and_le ne_s hf
  ⟨x, hxs, hx⟩
Existence of Infimum-Attaining Point for Continuous Function on Compact Set in `ClosedIicTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property (i.e., for every $a \in \alpha$, the set $\{x \in \alpha \mid x \leq a\}$ is closed). Let $s$ be a nonempty compact subset of a topological space $\beta$, and $f : \beta \to \alpha$ a function continuous on $s$. Then there exists a point $x \in s$ such that the infimum of $f$ over $s$ is achieved at $x$, i.e., $\inf f(s) = f(x)$.
IsCompact.exists_sSup_image_eq theorem
[ClosedIciTopology α] {s : Set β} (hs : IsCompact s) (ne_s : s.Nonempty) : ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, sSup (f '' s) = f x
Full source 
theorem IsCompact.exists_sSup_image_eq [ClosedIciTopology α] {s : Set β} (hs : IsCompact s)
    (ne_s : s.Nonempty) : ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, sSup (f '' s) = f x :=
  IsCompact.exists_sInf_image_eq (α := αᵒᵈ) hs ne_s
Supremum-Attaining Theorem for Continuous Functions on Compact Sets in `ClosedIciTopology` Spaces
Informal description
Let $\alpha$ be a topological space with a preorder where all upper intervals $[a, \infty)$ are closed, and let $\beta$ be another topological space. For any nonempty compact subset $s \subseteq \beta$ and any continuous function $f : \beta \to \alpha$ defined on $s$, there exists a point $x \in s$ such that the supremum of $f$ over $s$ is achieved at $x$, i.e., $\sup f(s) = f(x)$.
IsCompact.exists_isMinOn_mem_subset theorem
[ClosedIicTopology α] {f : β → α} {s t : Set β} {z : β} (ht : IsCompact t) (hf : ContinuousOn f t) (hz : z ∈ t) (hfz : ∀ z' ∈ t \ s, f z < f z') : ∃ x ∈ s, IsMinOn f t x
Full source 
theorem IsCompact.exists_isMinOn_mem_subset [ClosedIicTopology α] {f : β → α} {s t : Set β}
    {z : β} (ht : IsCompact t) (hf : ContinuousOn f t) (hz : z ∈ t)
    (hfz : ∀ z' ∈ t \ s, f z < f z') : ∃ x ∈ s, IsMinOn f t x :=
  let ⟨x, hxt, hfx⟩ := ht.exists_isMinOn ⟨z, hz⟩ hf
  ⟨x, by_contra fun hxs => (hfz x ⟨hxt, hxs⟩).not_le (hfx hz), hfx⟩
Existence of Minimum in Subset for Continuous Functions on Compact Sets
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be another topological space. Given a compact set $t \subseteq \beta$, a continuous function $f : \beta \to \alpha$ on $t$, and a point $z \in t$ such that $f(z) < f(z')$ for all $z' \in t \setminus s$, there exists a point $x \in s$ that minimizes $f$ on $t$, i.e., $f(x) \leq f(y)$ for all $y \in t$.
IsCompact.exists_isMaxOn_mem_subset theorem
[ClosedIciTopology α] {f : β → α} {s t : Set β} {z : β} (ht : IsCompact t) (hf : ContinuousOn f t) (hz : z ∈ t) (hfz : ∀ z' ∈ t \ s, f z' < f z) : ∃ x ∈ s, IsMaxOn f t x
Full source 
theorem IsCompact.exists_isMaxOn_mem_subset [ClosedIciTopology α] {f : β → α} {s t : Set β}
    {z : β} (ht : IsCompact t) (hf : ContinuousOn f t) (hz : z ∈ t)
    (hfz : ∀ z' ∈ t \ s, f z' < f z) : ∃ x ∈ s, IsMaxOn f t x :=
  let ⟨x, hxt, hfx⟩ := ht.exists_isMaxOn ⟨z, hz⟩ hf
  ⟨x, by_contra fun hxs => (hfz x ⟨hxt, hxs⟩).not_le (hfx hz), hfx⟩
Existence of Maximum in Subset for Continuous Functions on Compact Sets (Extreme Value Theorem Variant)
Informal description
Let $\alpha$ be a topological space with a preorder where all upper intervals $[a, \infty)$ are closed, and let $\beta$ be another topological space. Given a compact set $t \subseteq \beta$, a continuous function $f : \beta \to \alpha$ defined on $t$, a point $z \in t$, and the condition that $f(z') < f(z)$ for all $z' \in t \setminus s$, there exists a point $x \in s$ such that $f(x) \geq f(y)$ for all $y \in t$.
IsCompact.exists_isLocalMin_mem_open theorem
[ClosedIicTopology α] {f : β → α} {s 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) : ∃ x ∈ s, IsLocalMin f x
Full source 
theorem IsCompact.exists_isLocalMin_mem_open [ClosedIicTopology α] {f : β → α} {s 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) : ∃ x ∈ s, IsLocalMin f x :=
  let ⟨x, hxs, h⟩ := ht.exists_isMinOn_mem_subset hf hz hfz
  ⟨x, hxs, h.isLocalMin <| mem_nhds_iff.2 ⟨s, hst, hs, hxs⟩⟩
Existence of Local Minimum in Open Subset for Continuous Functions on Compact Sets
Informal description
Let $\alpha$ be a topological space with a preorder and the `ClosedIicTopology` property, and let $\beta$ be another topological space. Given a compact set $t \subseteq \beta$, an open subset $s \subseteq t$, a continuous function $f : \beta \to \alpha$ on $t$, and a point $z \in t$ such that $f(z) < f(z')$ for all $z' \in t \setminus s$, there exists a point $x \in s$ that is a local minimum of $f$.
IsCompact.exists_isLocalMax_mem_open theorem
[ClosedIciTopology α] {f : β → α} {s 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) : ∃ x ∈ s, IsLocalMax f x
Full source 
theorem IsCompact.exists_isLocalMax_mem_open [ClosedIciTopology α] {f : β → α} {s 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) : ∃ x ∈ s, IsLocalMax f x :=
  let ⟨x, hxs, h⟩ := ht.exists_isMaxOn_mem_subset hf hz hfz
  ⟨x, hxs, h.isLocalMax <| mem_nhds_iff.2 ⟨s, hst, hs, hxs⟩⟩
Existence of Local Maximum in Open Subset for Continuous Functions on Compact Sets
Informal description
Let $\alpha$ be a topological space with a preorder where all upper intervals $[a, \infty)$ are closed, and let $\beta$ be another topological space. Given a compact set $t \subseteq \beta$, an open subset $s \subseteq t$, a continuous function $f : \beta \to \alpha$ on $t$, and a point $z \in t$ such that $f(z') < f(z)$ for all $z' \in t \setminus s$, there exists a point $x \in s$ that is a local maximum of $f$.
IsCompact.continuous_sSup theorem
{f : γ → β → α} {K : Set β} (hK : IsCompact K) (hf : Continuous ↿f) : Continuous fun x => sSup (f x '' K)
Full source 
/-- 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. -/
/- TODO: generalize. The following version seems to be true:
```
theorem IsCompact.tendsto_sSup {f : γ → β → α} {g : β → α} {K : Set β} {l : Filter γ}
    (hK : IsCompact K) (hf : ∀ y ∈ K, Tendsto ↿f (l ×ˢ 𝓝[K] y) (𝓝 (g y)))
    (hgc : ContinuousOn g K) :
    Tendsto (fun x => sSup (f x '' K)) l (𝓝 (sSup (g '' K))) := _
```
Moreover, it seems that `hgc` follows from `hf` (Yury Kudryashov). -/
theorem IsCompact.continuous_sSup {f : γ → β → α} {K : Set β} (hK : IsCompact K)
    (hf : Continuous ↿f) : Continuous fun x => sSup (f x '' K) := by
  rcases eq_empty_or_nonempty K with (rfl | h0K)
  · simp_rw [image_empty]
    exact continuous_const
  rw [continuous_iff_continuousAt]
  intro x
  obtain ⟨y, hyK, h2y, hy⟩ :=
    hK.exists_sSup_image_eq_and_ge h0K
      (show Continuous (f x) from hf.comp <| .prodMk_right x).continuousOn
  rw [ContinuousAt, h2y, tendsto_order]
  have := tendsto_order.mp ((show Continuous fun x => f x y
    from hf.comp <| .prodMk_left _).tendsto x)
  refine ⟨fun z hz => ?_, fun z hz => ?_⟩
  · refine (this.1 z hz).mono fun x' hx' =>
      hx'.trans_le <| le_csSup ?_ <| mem_image_of_mem (f x') hyK
    exact hK.bddAbove_image (hf.comp <| .prodMk_right x').continuousOn
  · have h : ({x} : Set γ) ×ˢ K ⊆ ↿f ⁻¹' Iio z := by
      rintro ⟨x', y'⟩ ⟨(rfl : x' = x), hy'⟩
      exact (hy y' hy').trans_lt hz
    obtain ⟨u, v, hu, _, hxu, hKv, huv⟩ :=
      generalized_tube_lemma isCompact_singleton hK (isOpen_Iio.preimage hf) h
    refine eventually_of_mem (hu.mem_nhds (singleton_subset_iff.mp hxu)) fun x' hx' => ?_
    rw [hK.sSup_lt_iff_of_continuous h0K
        (show Continuous (f x') from hf.comp <| .prodMk_right x').continuousOn]
    exact fun y' hy' => huv (mk_mem_prod hx' (hKv hy'))
Continuity of Supremum Function over Compact Set
Informal description
Let $\alpha$ be a conditionally complete linear order with the order topology, $\beta$ and $\gamma$ be topological spaces, $K \subseteq \beta$ a compact set, and $f : \gamma \times \beta \to \alpha$ a continuous function. Then the function $g : \gamma \to \alpha$ defined by $g(x) = \sup \{f(x,y) \mid y \in K\}$ is continuous.
IsCompact.continuous_sInf theorem
{f : γ → β → α} {K : Set β} (hK : IsCompact K) (hf : Continuous ↿f) : Continuous fun x => sInf (f x '' K)
Full source 
theorem IsCompact.continuous_sInf {f : γ → β → α} {K : Set β} (hK : IsCompact K)
    (hf : Continuous ↿f) : Continuous fun x => sInf (f x '' K) :=
  IsCompact.continuous_sSup (α := αᵒᵈ) hK hf
Continuity of Infimum Function over Compact Set
Informal description
Let $\alpha$ be a conditionally complete linear order with the order topology, $\beta$ and $\gamma$ be topological spaces, $K \subseteq \beta$ a compact set, and $f : \gamma \times \beta \to \alpha$ a continuous function. Then the function $g : \gamma \to \alpha$ defined by $g(x) = \inf \{f(x,y) \mid y \in K\}$ is continuous.
ContinuousOn.image_Icc theorem
(hab : a ≤ b) (h : ContinuousOn f <| Icc a b) : f '' Icc a b = Icc (sInf <| f '' Icc a b) (sSup <| f '' Icc a b)
Full source 
theorem image_Icc (hab : a ≤ b) (h : ContinuousOn f <| Icc a b) :
    f '' Icc a b = Icc (sInf <| f '' Icc a b) (sSup <| f '' Icc a b) :=
  eq_Icc_of_connected_compact ⟨(nonempty_Icc.2 hab).image f, isPreconnected_Icc.image f h⟩
    (isCompact_Icc.image_of_continuousOn h)
Image of Closed Interval under Continuous Function is Closed Interval
Informal description
Let $f$ be a function defined on a closed interval $[a, b]$ in a conditionally complete linear order with the order topology, where $a \leq b$. If $f$ is continuous on $[a, b]$, then the image of $[a, b]$ under $f$ is the closed interval $[\inf f([a, b]), \sup f([a, b])]$.
ContinuousOn.image_uIcc_eq_Icc theorem
(h : ContinuousOn f [[a, b]]) : f '' [[a, b]] = Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
Full source 
theorem image_uIcc_eq_Icc (h : ContinuousOn f [[a, b]]) :
    f '' [[a, b]] = Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])) :=
  image_Icc min_le_max h
Image of Unordered Closed Interval under Continuous Function is Closed Interval
Informal description
Let $f$ be a continuous function on the unordered closed interval $[[a, b]]$ in a conditionally complete linear order with the order topology. Then the image of $[[a, b]]$ under $f$ is equal to the closed interval $[\inf f([[a, b]]), \sup f([[a, b]])]$.
ContinuousOn.image_uIcc theorem
(h : ContinuousOn f <| [[a, b]]) : f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
Full source 
theorem image_uIcc (h : ContinuousOn f <| [[a, b]]) :
    f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]] := by
  refine h.image_uIcc_eq_Icc.trans (uIcc_of_le ?_).symm
  refine csInf_le_csSup ?_ ?_ (nonempty_uIcc.image _) <;> rw [h.image_uIcc_eq_Icc]
  exacts [bddBelow_Icc, bddAbove_Icc]
Image of Unordered Closed Interval under Continuous Function is Unordered Closed Interval
Informal description
Let $f$ be a continuous function on the unordered closed interval $[[a, b]] := [\min(a,b), \max(a,b)]$ in a conditionally complete linear order with the order topology. Then the image of $[[a, b]]$ under $f$ is equal to the unordered closed interval $[[\inf f([[a, b]]), \sup f([[a, b]])]]$.
ContinuousOn.sInf_image_Icc_le theorem
(h : ContinuousOn f <| Icc a b) (hc : c ∈ Icc a b) : sInf (f '' Icc a b) ≤ f c
Full source 
theorem sInf_image_Icc_le (h : ContinuousOn f <| Icc a b) (hc : c ∈ Icc a b) :
    sInf (f '' Icc a b) ≤ f c := by
  have := mem_image_of_mem f hc
  rw [h.image_Icc (hc.1.trans hc.2)] at this
  exact this.1
Infimum of Continuous Function on Closed Interval Bounds All Values
Informal description
Let $f$ be a continuous function on the closed interval $[a, b]$ in a conditionally complete linear order with the order topology, where $a \leq b$. For any point $c \in [a, b]$, the infimum of the image of $[a, b]$ under $f$ is less than or equal to $f(c)$. In other words, $\inf f([a, b]) \leq f(c)$ for all $c \in [a, b]$.
ContinuousOn.le_sSup_image_Icc theorem
(h : ContinuousOn f <| Icc a b) (hc : c ∈ Icc a b) : f c ≤ sSup (f '' Icc a b)
Full source 
theorem le_sSup_image_Icc (h : ContinuousOn f <| Icc a b) (hc : c ∈ Icc a b) :
    f c ≤ sSup (f '' Icc a b) := by
  have := mem_image_of_mem f hc
  rw [h.image_Icc (hc.1.trans hc.2)] at this
  exact this.2
Upper Bound Property for Continuous Functions on Closed Intervals
Informal description
Let $f$ be a continuous function on the closed interval $[a, b]$ in a conditionally complete linear order with the order topology, and let $c \in [a, b]$. Then $f(c) \leq \sup f([a, b])$.