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.
A closed interval
Set.Icc a bis a compact set for allaandb.
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
theorem
CompactIccSpace.mk'
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
(h : ∀ {a b : α}, a ≤ b → IsCompact (Set.Icc a b))
:
theorem
CompactIccSpace.mk''
{α : Type u_1}
[TopologicalSpace α]
[PartialOrder α]
(h : ∀ {a b : α}, a < b → IsCompact (Set.Icc a b))
:
instance
ConditionallyCompleteLinearOrder.toCompactIccSpace
(α : Type u_1)
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
:
A closed interval in a conditionally complete linear order is compact.
instance
instCompactIccSpaceForAllTopologicalSpacePreorder
{ι : Type u_1}
{α : ι → Type u_2}
[(i : ι) → Preorder (α i)]
[(i : ι) → TopologicalSpace (α i)]
[∀ (i : ι), CompactIccSpace (α i)]
:
CompactIccSpace ((i : ι) → α i)
instance
Pi.compact_Icc_space'
{α : Type u_1}
{β : Type u_2}
[Preorder β]
[TopologicalSpace β]
[CompactIccSpace β]
:
CompactIccSpace (α → β)
instance
instCompactIccSpaceProdInstTopologicalSpaceProdInstPreorderProd
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
[Preorder β]
[TopologicalSpace β]
[CompactIccSpace β]
:
CompactIccSpace (α × β)
theorem
isCompact_uIcc
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[CompactIccSpace α]
{a : α}
{b : α}
:
An unordered closed interval is compact.
instance
compactSpace_of_completeLinearOrder
{α : Type u_1}
[CompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
:
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
compactSpace_Icc
{α : Type u_1}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
(a : α)
(b : α)
:
CompactSpace ↑(Set.Icc a b)
Equations
Extreme value theorem #
theorem
IsCompact.exists_isLeast
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
∃ x, IsLeast s x
theorem
IsCompact.exists_isGreatest
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
∃ x, IsGreatest s x
theorem
IsCompact.exists_isGLB
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.exists_isLUB
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.exists_isMinOn
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
The extreme value theorem: a continuous function realizes its minimum on a compact set.
@[deprecated IsCompact.exists_isMinOn]
theorem
IsCompact.exists_forall_le
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
The extreme value theorem: a continuous function realizes its minimum on a compact set.
theorem
IsCompact.exists_isMaxOn
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
The extreme value theorem: a continuous function realizes its maximum on a compact set.
@[deprecated IsCompact.exists_isMaxOn]
theorem
IsCompact.exists_forall_ge
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
The extreme value theorem: a continuous function realizes its maximum on a compact set.
theorem
ContinuousOn.exists_isMinOn'
{α : Type u_1}
{β : Type u_2}
[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)
:
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.
@[deprecated ContinuousOn.exists_isMinOn']
theorem
ContinuousOn.exists_forall_le'
{α : Type u_1}
{β : Type u_2}
[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)
:
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_1}
{β : Type u_2}
[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₀)
:
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.
@[deprecated ContinuousOn.exists_isMaxOn']
theorem
ContinuousOn.exists_forall_ge'
{α : Type u_1}
{β : Type u_2}
[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₀)
:
The extreme value theorem: if a function f is continuous on a closed set s and it is
smaller than a value in its image away from compact sets, then it has a maximum on this set.
theorem
Continuous.exists_forall_le'
{α : Type u_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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_1}
{β : Type u_2}
[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_1}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
[Nonempty α]
{s : Set α}
(hs : IsCompact s)
:
BddBelow s
A compact set is bounded below
theorem
IsCompact.bddAbove
{α : Type u_1}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
[Nonempty α]
{s : Set α}
(hs : IsCompact s)
:
BddAbove s
A compact set is bounded above
theorem
IsCompact.bddBelow_image
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
[Nonempty α]
{f : β → α}
{K : Set β}
(hK : IsCompact K)
(hf : ContinuousOn f K)
:
A continuous function is bounded below on a compact set.
theorem
IsCompact.bddAbove_image
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
[Nonempty α]
{f : β → α}
{K : Set β}
(hK : IsCompact K)
(hf : ContinuousOn f K)
:
A continuous function is bounded above on a compact set.
theorem
Continuous.bddBelow_range_of_hasCompactSupport
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
[Zero α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactSupport f)
:
A continuous function with compact support is bounded below.
theorem
Continuous.bddBelow_range_of_hasCompactMulSupport
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
[One α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactMulSupport f)
:
A continuous function with compact support is bounded below.
theorem
Continuous.bddAbove_range_of_hasCompactSupport
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
[Zero α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactSupport f)
:
A continuous function with compact support is bounded above.
theorem
Continuous.bddAbove_range_of_hasCompactMulSupport
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
[One α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactMulSupport f)
:
A continuous function with compact support is bounded above.
theorem
IsCompact.sSup_lt_iff_of_continuous
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{f : β → α}
{K : Set β}
(hK : IsCompact K)
(h0K : Set.Nonempty K)
(hf : ContinuousOn f K)
(y : α)
:
theorem
IsCompact.lt_sInf_iff_of_continuous
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{f : β → α}
{K : Set β}
(hK : IsCompact K)
(h0K : Set.Nonempty K)
(hf : ContinuousOn f K)
(y : α)
:
Min and max elements of a compact set #
theorem
IsCompact.sInf_mem
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.sSup_mem
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.isGLB_sInf
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.isLUB_sSup
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.isLeast_sInf
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.isGreatest_sSup
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
IsGreatest s (sSup s)
theorem
IsCompact.exists_sInf_image_eq_and_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
theorem
IsCompact.exists_sSup_image_eq_and_ge
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
theorem
IsCompact.exists_sInf_image_eq
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
theorem
IsCompact.exists_sSup_image_eq
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
:
theorem
IsCompact.exists_isMinOn_mem_subset
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{f : β → α}
{s : Set β}
{t : Set β}
{z : β}
(ht : IsCompact t)
(hf : ContinuousOn f t)
(hz : z ∈ t)
(hfz : ∀ (z' : β), z' ∈ t \ s → f z < f z')
:
theorem
IsCompact.exists_isMaxOn_mem_subset
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{f : β → α}
{s : Set β}
{t : Set β}
{z : β}
(ht : IsCompact t)
(hf : ContinuousOn f t)
(hz : z ∈ t)
(hfz : ∀ (z' : β), z' ∈ t \ s → f z' < f z)
:
@[deprecated IsCompact.exists_isMinOn_mem_subset]
theorem
IsCompact.exists_isLocalMinOn_mem_subset
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{f : β → α}
{s : Set β}
{t : Set β}
{z : β}
(ht : IsCompact t)
(hf : ContinuousOn f t)
(hz : z ∈ t)
(hfz : ∀ (z' : β), z' ∈ t \ s → f z < f z')
:
∃ x, x ∈ s ∧ IsLocalMinOn f t x
theorem
IsCompact.exists_isLocalMin_mem_open
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{f : β → α}
{s : Set β}
{t : Set β}
{z : β}
(ht : IsCompact t)
(hst : s ⊆ t)
(hf : ContinuousOn f t)
(hz : z ∈ t)
(hfz : ∀ (z' : β), z' ∈ t \ s → f z < f z')
(hs : IsOpen s)
:
∃ x, x ∈ s ∧ IsLocalMin f x
theorem
IsCompact.exists_isLocalMax_mem_open
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{f : β → α}
{s : Set β}
{t : Set β}
{z : β}
(ht : IsCompact t)
(hst : s ⊆ t)
(hf : ContinuousOn f t)
(hz : z ∈ t)
(hfz : ∀ (z' : β), z' ∈ t \ s → f z' < f z)
(hs : IsOpen s)
:
∃ x, x ∈ s ∧ IsLocalMax f x
theorem
eq_Icc_of_connected_compact
{α : Type u_1}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{s : Set α}
(h₁ : IsConnected s)
(h₂ : IsCompact s)
:
theorem
IsCompact.continuous_sSup
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[TopologicalSpace γ]
{f : γ → β → α}
{K : Set β}
(hK : IsCompact K)
(hf : Continuous ↿f)
:
Continuous fun x => sSup (f x '' K)
theorem
IsCompact.continuous_sInf
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[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_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[DenselyOrdered α]
[ConditionallyCompleteLinearOrder β]
[OrderTopology β]
{f : α → β}
{a : α}
{b : α}
(hab : a ≤ b)
(h : ContinuousOn f (Set.Icc a b))
:
theorem
ContinuousOn.image_uIcc_eq_Icc
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[DenselyOrdered α]
[ConditionallyCompleteLinearOrder β]
[OrderTopology β]
{f : α → β}
{a : α}
{b : α}
(h : ContinuousOn f (Set.uIcc a b))
:
theorem
ContinuousOn.image_uIcc
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[DenselyOrdered α]
[ConditionallyCompleteLinearOrder β]
[OrderTopology β]
{f : α → β}
{a : α}
{b : α}
(h : ContinuousOn f (Set.uIcc a b))
:
theorem
ContinuousOn.sInf_image_Icc_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[DenselyOrdered α]
[ConditionallyCompleteLinearOrder β]
[OrderTopology β]
{f : α → β}
{a : α}
{b : α}
{c : α}
(h : ContinuousOn f (Set.Icc a b))
(hc : c ∈ Set.Icc a b)
:
theorem
ContinuousOn.le_sSup_image_Icc
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[DenselyOrdered α]
[ConditionallyCompleteLinearOrder β]
[OrderTopology β]
{f : α → β}
{a : α}
{b : α}
{c : α}
(h : ContinuousOn f (Set.Icc a b))
(hc : c ∈ Set.Icc a b)
: