Compactness of a closed interval #
In this file we prove that a closed interval in a conditionally complete linear ordered type with order topology (or a product of such types) is compact.
We prove the extreme value theorem (IsCompact.exists_isMinOn, IsCompact.exists_isMaxOn):
a continuous function on a compact set takes its minimum and maximum values. We provide many
variations of this theorem.
We also prove that the image of a closed interval under a continuous map is a closed interval, see
ContinuousOn.image_Icc.
Tags #
compact, extreme value theorem
Compactness of a closed interval #
In this section we define a typeclass CompactIccSpace α saying that all closed intervals in α
are compact. Then we provide an instance for a ConditionallyCompleteLinearOrder and prove that
the product (both α × β and an indexed product) of spaces with this property inherits the
property.
We also prove some simple lemmas about spaces with this property.
This typeclass says that all closed intervals in α are compact. This is true for all
conditionally complete linear orders with order topology and products (finite or infinite)
of such spaces.
A closed interval
Set.Icc a bis a compact set for allaandb.
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
instCompactIccSpaceOrderDualInstTopologicalSpaceOrderDualInstPreorder
{α : Type u_1}
[TopologicalSpace α]
[Preorder α]
[CompactIccSpace α]
:
Equations
- ⋯ = ⋯
instance
ConditionallyCompleteLinearOrder.toCompactIccSpace
(α : Type u_2)
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
:
A closed interval in a conditionally complete linear order is compact.
Equations
- ⋯ = ⋯
instance
instCompactIccSpaceForAllTopologicalSpacePreorder
{ι : Type u_2}
{α : ι → Type u_3}
[(i : ι) → Preorder (α i)]
[(i : ι) → TopologicalSpace (α i)]
[∀ (i : ι), CompactIccSpace (α i)]
:
CompactIccSpace ((i : ι) → α i)
Equations
- ⋯ = ⋯
instance
Pi.compact_Icc_space'
{α : Type u_2}
{β : Type u_3}
[Preorder β]
[TopologicalSpace β]
[CompactIccSpace β]
:
CompactIccSpace (α → β)
Equations
- ⋯ = ⋯
instance
instCompactIccSpaceProdInstTopologicalSpaceProdInstPreorderProd
{α : Type u_2}
{β : Type u_3}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
[Preorder β]
[TopologicalSpace β]
[CompactIccSpace β]
:
CompactIccSpace (α × β)
Equations
- ⋯ = ⋯
theorem
isCompact_uIcc
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[CompactIccSpace α]
{a : α}
{b : α}
:
An unordered closed interval is compact.
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.
Equations
- ⋯ = ⋯
instance
compactSpace_Icc
{α : Type u_2}
[Preorder α]
[TopologicalSpace α]
[CompactIccSpace α]
(a : α)
(b : α)
:
CompactSpace ↑(Set.Icc a b)
Equations
- ⋯ = ⋯
Extreme value theorem #
theorem
IsCompact.exists_isLeast
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
∃ (x : α), IsLeast s x
theorem
IsCompact.exists_isGreatest
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
∃ (x : α), IsGreatest s x
theorem
IsCompact.exists_isGLB
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
∃ x ∈ s, IsGLB s x
theorem
IsCompact.exists_isLUB
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
∃ x ∈ s, IsLUB s x
theorem
cocompact_le_atBot_atTop
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[CompactIccSpace α]
:
Filter.cocompact α ≤ Filter.atBot ⊔ Filter.atTop
theorem
cocompact_le_atBot
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[OrderTop α]
[CompactIccSpace α]
:
Filter.cocompact α ≤ Filter.atBot
theorem
cocompact_le_atTop
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[OrderBot α]
[CompactIccSpace α]
:
Filter.cocompact α ≤ Filter.atTop
theorem
atBot_le_cocompact
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMinOrder α]
[ClosedIicTopology α]
:
Filter.atBot ≤ Filter.cocompact α
theorem
atTop_le_cocompact
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMaxOrder α]
[ClosedIciTopology α]
:
Filter.atTop ≤ Filter.cocompact α
theorem
atBot_atTop_le_cocompact
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMinOrder α]
[NoMaxOrder α]
[OrderClosedTopology α]
:
Filter.atBot ⊔ Filter.atTop ≤ Filter.cocompact α
@[simp]
theorem
cocompact_eq_atBot_atTop
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMaxOrder α]
[NoMinOrder α]
[OrderClosedTopology α]
[CompactIccSpace α]
:
Filter.cocompact α = Filter.atBot ⊔ Filter.atTop
@[simp]
theorem
cocompact_eq_atBot
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMinOrder α]
[OrderTop α]
[ClosedIicTopology α]
[CompactIccSpace α]
:
Filter.cocompact α = Filter.atBot
@[simp]
theorem
cocompact_eq_atTop
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[NoMaxOrder α]
[OrderBot α]
[ClosedIciTopology α]
[CompactIccSpace α]
:
Filter.cocompact α = Filter.atTop
theorem
IsCompact.exists_isMinOn
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{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.
@[deprecated IsCompact.exists_isMinOn]
theorem
IsCompact.exists_forall_le
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
∃ x ∈ s, ∀ y ∈ s, f x ≤ f y
The extreme value theorem: a continuous function realizes its minimum on a compact set.
theorem
IsCompact.exists_isMaxOn
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{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.
@[deprecated IsCompact.exists_isMaxOn]
theorem
IsCompact.exists_forall_ge
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{f : β → α}
(hf : ContinuousOn f s)
:
∃ x ∈ s, ∀ y ∈ s, f y ≤ f 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.
@[deprecated ContinuousOn.exists_isMinOn']
theorem
ContinuousOn.exists_forall_le'
{α : 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, ∀ y ∈ s, f x ≤ f y
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.
@[deprecated ContinuousOn.exists_isMaxOn']
theorem
ContinuousOn.exists_forall_ge'
{α : 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, ∀ y ∈ s, f y ≤ 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_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{f : β → α}
(hf : Continuous f)
(x₀ : β)
(h : ∀ᶠ (x : β) in Filter.cocompact β, f x₀ ≤ f x)
:
∃ (x : β), ∀ (y : β), f x ≤ f y
The extreme value theorem: if a continuous function f is larger than a value in its range
away from compact sets, then it has a global minimum.
theorem
Continuous.exists_forall_ge'
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{f : β → α}
(hf : Continuous f)
(x₀ : β)
(h : ∀ᶠ (x : β) in Filter.cocompact β, f x ≤ f x₀)
:
∃ (x : β), ∀ (y : β), f y ≤ f x
The extreme value theorem: if a continuous function f is smaller than a value in its range
away from compact sets, then it has a global maximum.
theorem
Continuous.exists_forall_le
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
[Nonempty β]
{f : β → α}
(hf : Continuous f)
(hlim : Filter.Tendsto f (Filter.cocompact β) Filter.atTop)
:
∃ (x : β), ∀ (y : β), f x ≤ f y
The extreme value theorem: if a continuous function f tends to infinity away from compact
sets, then it has a global minimum.
theorem
Continuous.exists_forall_ge
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
[Nonempty β]
{f : β → α}
(hf : Continuous f)
(hlim : Filter.Tendsto f (Filter.cocompact β) Filter.atBot)
:
∃ (x : β), ∀ (y : β), f y ≤ f x
The extreme value theorem: if a continuous function f tends to negative infinity away from
compact sets, then it has a global maximum.
theorem
Continuous.exists_forall_le_of_hasCompactSupport
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
[Nonempty β]
[Zero α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactSupport f)
:
∃ (x : β), ∀ (y : β), f x ≤ f y
A continuous function with compact support has a global minimum.
theorem
Continuous.exists_forall_le_of_hasCompactMulSupport
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
[Nonempty β]
[One α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactMulSupport f)
:
∃ (x : β), ∀ (y : β), f x ≤ f y
A continuous function with compact support has a global minimum.
theorem
Continuous.exists_forall_ge_of_hasCompactSupport
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
[Nonempty β]
[Zero α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactSupport f)
:
∃ (x : β), ∀ (y : β), f y ≤ f x
A continuous function with compact support has a global maximum.
theorem
Continuous.exists_forall_ge_of_hasCompactMulSupport
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
[Nonempty β]
[One α]
{f : β → α}
(hf : Continuous f)
(h : HasCompactMulSupport f)
:
∃ (x : β), ∀ (y : β), f y ≤ f x
A continuous function with compact support has a global maximum.
theorem
IsCompact.bddBelow
{α : Type u_2}
[LinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
[Nonempty α]
{s : Set α}
(hs : IsCompact s)
:
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_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.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.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
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
IsCompact.sSup_lt_iff_of_continuous
{α : Type u_2}
{β : Type u_3}
[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_2}
{β : Type u_3}
[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_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.sSup_mem
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.isGLB_sInf
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.isLUB_sSup
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIciTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.isLeast_sInf
{α : Type u_2}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[ClosedIicTopology α]
{s : Set α}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
:
theorem
IsCompact.isGreatest_sSup
{α : Type u_2}
[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_2}
{β : Type u_3}
[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_2}
{β : Type u_3}
[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_2}
{β : Type u_3}
[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_2}
{β : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{s : Set β}
(hs : IsCompact s)
(ne_s : Set.Nonempty s)
{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 : Set β}
{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 : Set β}
{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
@[deprecated IsCompact.exists_isMinOn_mem_subset]
theorem
IsCompact.exists_isLocalMinOn_mem_subset
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{f : β → α}
{s : Set β}
{t : Set β}
{z : β}
(ht : IsCompact t)
(hf : ContinuousOn f t)
(hz : z ∈ t)
(hfz : ∀ z' ∈ t \ s, f z < f z')
:
∃ x ∈ s, IsLocalMinOn f t x
theorem
IsCompact.exists_isLocalMin_mem_open
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIicTopology α]
{f : β → α}
{s : Set β}
{t : Set β}
{z : β}
(ht : IsCompact t)
(hst : s ⊆ t)
(hf : ContinuousOn f t)
(hz : z ∈ t)
(hfz : ∀ z' ∈ t \ s, f z < f z')
(hs : IsOpen s)
:
∃ x ∈ s, IsLocalMin f x
theorem
IsCompact.exists_isLocalMax_mem_open
{α : Type u_2}
{β : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[TopologicalSpace β]
[ClosedIciTopology α]
{f : β → α}
{s : Set β}
{t : Set β}
{z : β}
(ht : IsCompact t)
(hst : s ⊆ t)
(hf : ContinuousOn f t)
(hz : z ∈ t)
(hfz : ∀ z' ∈ t \ s, f z' < f z)
(hs : IsOpen s)
:
∃ 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)
: