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.
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
instCompactIccSpaceOrderDual
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
[CompactIccSpace α]
:
@[instance 100]
instance
ConditionallyCompleteLinearOrder.toCompactIccSpace
(α : Type u_2)
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
:
A closed interval in a conditionally complete linear order is compact.
instance
instCompactIccSpaceForall
{ι : Type u_2}
{α : ι → Type u_3}
[(i : ι) → Preorder (α i)]
[(i : ι) → TopologicalSpace (α i)]
[∀ (i : ι), CompactIccSpace (α i)]
:
CompactIccSpace ((i : ι) → α i)
instance
Pi.compact_Icc_space'
{α : Type u_2}
{β : Type u_3}
[Preorder β]
[TopologicalSpace β]
[CompactIccSpace β]
:
CompactIccSpace (α → β)
instance
instCompactIccSpaceProd
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
[Preorder β]
[TopologicalSpace β]
[CompactIccSpace β]
:
CompactIccSpace (α × β)
theorem
isCompact_uIcc
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[CompactIccSpace α]
{a b : α}
:
An unordered closed interval is compact.
@[instance 100]
instance
compactSpace_of_completeLinearOrder
{α : Type u_2}
[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_2}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
(a b : α)
:
CompactSpace ↑(Set.Icc a b)
@[simp]
theorem
isCompact_Ico_iff
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
:
Set.Ico a b is only compact if it is empty.
@[simp]
theorem
isCompact_Ioc_iff
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
:
Set.Ioc a b is only compact if it is empty.
@[simp]
theorem
isCompact_Ioo_iff
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[DenselyOrdered α]
{a b : α}
:
Set.Ioo a b is only compact if it is empty.
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)
:
∃ x ∈ s, IsGLB s x
theorem
IsCompact.exists_isLUB
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : s.Nonempty)
:
∃ x ∈ s, IsLUB s x
theorem
cocompact_le_atBot_atTop
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[CompactIccSpace α]
:
theorem
cocompact_le_atBot
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[OrderTop α]
[CompactIccSpace α]
:
theorem
cocompact_le_atTop
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[OrderBot α]
[CompactIccSpace α]
:
theorem
atBot_le_cocompact
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMinOrder α]
[ClosedIicTopology α]
:
theorem
atTop_le_cocompact
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMaxOrder α]
[ClosedIciTopology α]
:
theorem
atBot_atTop_le_cocompact
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMinOrder α]
[NoMaxOrder α]
[OrderClosedTopology α]
:
@[simp]
theorem
cocompact_eq_atBot_atTop
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMaxOrder α]
[NoMinOrder α]
[OrderClosedTopology α]
[CompactIccSpace α]
:
@[simp]
theorem
cocompact_eq_atBot
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMinOrder α]
[OrderTop α]
[ClosedIicTopology α]
[CompactIccSpace α]
:
@[simp]
theorem
cocompact_eq_atTop
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMaxOrder α]
[OrderBot α]
[ClosedIciTopology α]
[CompactIccSpace α]
:
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)
:
∃ x ∈ s, 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' : ∀ b ∈ s, 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)
:
∃ x ∈ s, 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)
:
∃ x ∈ s, 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₀)
:
∃ x ∈ s, 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_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_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_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
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
IsCompact.bddBelow
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
[Nonempty α]
{s : Set α}
(hs : IsCompact s)
:
BddBelow s
A compact set is bounded below
theorem
IsCompact.bddAbove
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
[Nonempty α]
{s : Set α}
(hs : IsCompact s)
:
BddAbove 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)
:
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)
:
A continuous function is bounded above on a compact set.
theorem
Continuous.bddBelow_range_of_hasCompactMulSupport
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
[One α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactMulSupport f)
:
A continuous function with compact support is bounded below.
theorem
Continuous.bddBelow_range_of_hasCompactSupport
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
[Zero α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactSupport f)
:
A continuous function with compact support is bounded below.
theorem
Continuous.bddAbove_range_of_hasCompactMulSupport
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
[One α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactMulSupport f)
:
A continuous function with compact support is bounded above.
theorem
Continuous.bddAbove_range_of_hasCompactSupport
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
[Zero α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactSupport f)
:
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 : α)
:
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 : α)
:
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)
:
theorem
IsCompact.sSup_mem
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : s.Nonempty)
:
theorem
IsCompact.isGLB_sInf
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : s.Nonempty)
:
theorem
IsCompact.isLUB_sSup
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : s.Nonempty)
:
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)
:
IsGreatest s (sSup s)
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)
:
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)
:
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)
:
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 s → ∃ x ∈ s, sSup (f '' s) = f x
theorem
IsCompact.exists_isMinOn_mem_subset
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[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
theorem
IsCompact.exists_isMaxOn_mem_subset
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[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
theorem
IsCompact.exists_isLocalMin_mem_open
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[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
theorem
IsCompact.exists_isLocalMax_mem_open
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[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
theorem
eq_Icc_of_connected_compact
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
{s : Set α}
(h₁ : IsConnected s)
(h₂ : IsCompact s)
:
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))
:
theorem
ContinuousOn.image_uIcc_eq_Icc
{α : Type u_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[TopologicalSpace β]
[DenselyOrdered α]
[ConditionallyCompleteLinearOrder β]
[OrderTopology β]
{f : α → β}
{a b : α}
(h : ContinuousOn f (Set.uIcc 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))
:
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)
:
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)
:
theorem
ContinuousOn.image_Icc_of_monotoneOn
{α : 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))
(h' : MonotoneOn f (Set.Icc a b))
:
theorem
ContinuousOn.image_Icc_of_antitoneOn
{α : 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))
(h' : AntitoneOn f (Set.Icc a b))
: