Properties of LUB and GLB in an order topology #
theorem
IsLUB.frequently_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsLUB s a)
(hs : s.Nonempty)
:
theorem
IsLUB.frequently_nhds_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsLUB s a)
(hs : s.Nonempty)
:
theorem
IsGLB.frequently_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsGLB s a)
(hs : s.Nonempty)
:
theorem
IsGLB.frequently_nhds_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsGLB s a)
(hs : s.Nonempty)
:
theorem
IsLUB.mem_closure
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsLUB s a)
(hs : s.Nonempty)
:
theorem
IsGLB.mem_closure
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsGLB s a)
(hs : s.Nonempty)
:
theorem
IsLUB.nhdsWithin_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsLUB s a)
(hs : s.Nonempty)
:
(nhdsWithin a s).NeBot
theorem
IsGLB.nhdsWithin_neBot
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsGLB s a)
(hs : s.Nonempty)
:
(nhdsWithin a s).NeBot
theorem
isLUB_of_mem_nhds
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{s : Set α}
{a : α}
{f : Filter α}
(hsa : a ∈ upperBounds s)
(hsf : s ∈ f)
[(f ⊓ nhds a).NeBot]
:
IsLUB s a
theorem
isLUB_of_mem_closure
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{s : Set α}
{a : α}
(hsa : a ∈ upperBounds s)
(hsf : a ∈ closure s)
:
IsLUB s a
theorem
isGLB_of_mem_nhds
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{s : Set α}
{a : α}
{f : Filter α}
(hsa : a ∈ lowerBounds s)
(hsf : s ∈ f)
[(f ⊓ nhds a).NeBot]
:
IsGLB s a
theorem
isGLB_of_mem_closure
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{s : Set α}
{a : α}
(hsa : a ∈ lowerBounds s)
(hsf : a ∈ closure s)
:
IsGLB s a
theorem
IsLUB.mem_upperBounds_of_tendsto
{α : Type u_1}
{γ : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[Preorder γ]
[TopologicalSpace γ]
[OrderClosedTopology γ]
{f : α → γ}
{s : Set α}
{a : α}
{b : γ}
(hf : MonotoneOn f s)
(ha : IsLUB s a)
(hb : Filter.Tendsto f (nhdsWithin a s) (nhds b))
:
theorem
IsLUB.isLUB_of_tendsto
{α : Type u_1}
{γ : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[Preorder γ]
[TopologicalSpace γ]
[OrderClosedTopology γ]
{f : α → γ}
{s : Set α}
{a : α}
{b : γ}
(hf : MonotoneOn f s)
(ha : IsLUB s a)
(hs : s.Nonempty)
(hb : Filter.Tendsto f (nhdsWithin a s) (nhds b))
:
theorem
IsGLB.mem_lowerBounds_of_tendsto
{α : Type u_1}
{γ : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[Preorder γ]
[TopologicalSpace γ]
[OrderClosedTopology γ]
{f : α → γ}
{s : Set α}
{a : α}
{b : γ}
(hf : MonotoneOn f s)
(ha : IsGLB s a)
(hb : Filter.Tendsto f (nhdsWithin a s) (nhds b))
:
theorem
IsGLB.isGLB_of_tendsto
{α : Type u_1}
{γ : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[Preorder γ]
[TopologicalSpace γ]
[OrderClosedTopology γ]
{f : α → γ}
{s : Set α}
{a : α}
{b : γ}
(hf : MonotoneOn f s)
:
IsGLB s a → s.Nonempty → Filter.Tendsto f (nhdsWithin a s) (nhds b) → IsGLB (f '' s) b
theorem
IsLUB.mem_lowerBounds_of_tendsto
{α : Type u_1}
{γ : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[Preorder γ]
[TopologicalSpace γ]
[OrderClosedTopology γ]
{f : α → γ}
{s : Set α}
{a : α}
{b : γ}
(hf : AntitoneOn f s)
(ha : IsLUB s a)
(hb : Filter.Tendsto f (nhdsWithin a s) (nhds b))
:
theorem
IsLUB.isGLB_of_tendsto
{α : Type u_1}
{γ : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[Preorder γ]
[TopologicalSpace γ]
[OrderClosedTopology γ]
{f : α → γ}
{s : Set α}
{a : α}
{b : γ}
(hf : AntitoneOn f s)
(ha : IsLUB s a)
(hs : s.Nonempty)
(hb : Filter.Tendsto f (nhdsWithin a s) (nhds b))
:
theorem
IsGLB.mem_upperBounds_of_tendsto
{α : Type u_1}
{γ : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[Preorder γ]
[TopologicalSpace γ]
[OrderClosedTopology γ]
{f : α → γ}
{s : Set α}
{a : α}
{b : γ}
(hf : AntitoneOn f s)
(ha : IsGLB s a)
(hb : Filter.Tendsto f (nhdsWithin a s) (nhds b))
:
theorem
IsGLB.isLUB_of_tendsto
{α : Type u_1}
{γ : Type u_2}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[Preorder γ]
[TopologicalSpace γ]
[OrderClosedTopology γ]
{f : α → γ}
{s : Set α}
{a : α}
{b : γ}
(hf : AntitoneOn f s)
(ha : IsGLB s a)
(hs : s.Nonempty)
(hb : Filter.Tendsto f (nhdsWithin a s) (nhds b))
:
theorem
IsLUB.mem_of_isClosed
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsLUB s a)
(hs : s.Nonempty)
(sc : IsClosed s)
:
theorem
IsClosed.isLUB_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsLUB s a)
(hs : s.Nonempty)
(sc : IsClosed s)
:
Alias of IsLUB.mem_of_isClosed.
theorem
IsGLB.mem_of_isClosed
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsGLB s a)
(hs : s.Nonempty)
(sc : IsClosed s)
:
theorem
IsClosed.isGLB_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsGLB s a)
(hs : s.Nonempty)
(sc : IsClosed s)
:
Alias of IsGLB.mem_of_isClosed.
theorem
isLUB_iff_of_subset_of_subset_closure
{α : Type u_3}
[TopologicalSpace α]
[Preorder α]
[ClosedIicTopology α]
{s t : Set α}
(hst : s ⊆ t)
(hts : t ⊆ closure s)
{x : α}
:
theorem
isGLB_iff_of_subset_of_subset_closure
{α : Type u_3}
[TopologicalSpace α]
[Preorder α]
[ClosedIciTopology α]
{s t : Set α}
(hst : s ⊆ t)
(hts : t ⊆ closure s)
{x : α}
:
theorem
Dense.isLUB_inter_iff
{α : Type u_3}
[TopologicalSpace α]
[Preorder α]
[ClosedIicTopology α]
{s t : Set α}
(hs : Dense s)
(ht : IsOpen t)
{x : α}
:
theorem
Dense.isGLB_inter_iff
{α : Type u_3}
[TopologicalSpace α]
[Preorder α]
[ClosedIciTopology α]
{s t : Set α}
(hs : Dense s)
(ht : IsOpen t)
{x : α}
:
theorem
Dense.upperBounds_image
{γ : Type u_2}
{α : Type u_3}
[TopologicalSpace α]
[Preorder α]
[ClosedIicTopology α]
{f : γ → α}
[TopologicalSpace γ]
{S : Set γ}
(hS : Dense S)
(hf : Continuous f)
:
The upper bounds of the image of a continuous function on a dense set are equal to the upper bounds of the range of the universe.
theorem
Dense.lowerBounds_image
{γ : Type u_2}
{α : Type u_3}
[TopologicalSpace α]
[Preorder α]
[ClosedIciTopology α]
{f : γ → α}
[TopologicalSpace γ]
{S : Set γ}
(hS : Dense S)
(hf : Continuous f)
:
The lower bounds of the image of a continuous function on a dense set are equal to the lower bounds of the range of the universe.
theorem
Dense.ciSup
{γ : Type u_2}
{α : Type u_3}
[TopologicalSpace α]
[ConditionallyCompleteLattice α]
[ClosedIicTopology α]
{f : γ → α}
[TopologicalSpace γ]
{S : Set γ}
(hS : Dense S)
(hf : Continuous f)
(h : BddAbove (Set.range f))
:
The supremum of a bounded above, continuous function on a dense set is equal to the supremum on the universe.
theorem
Dense.ciInf
{γ : Type u_2}
{α : Type u_3}
[TopologicalSpace α]
[ConditionallyCompleteLattice α]
[ClosedIciTopology α]
{f : γ → α}
[TopologicalSpace γ]
{S : Set γ}
(hS : Dense S)
(hf : Continuous f)
(h : BddBelow (Set.range f))
:
The infimum of a bounded below, continuous function on a dense set is equal to the infimum on the universe.
theorem
Dense.ciSup'
{γ : Type u_2}
{α : Type u_3}
[TopologicalSpace α]
[ConditionallyCompleteLinearOrder α]
[ClosedIicTopology α]
{f : γ → α}
[TopologicalSpace γ]
{S : Set γ}
(hS : Dense S)
(hf : Continuous f)
:
This is an analogue of Dense.continuous_sup for functions taking values in a conditionally
complete linear order. The assumption of BddAbove (range f) is not needed in this theorem.
theorem
Dense.ciInf'
{γ : Type u_2}
{α : Type u_3}
[TopologicalSpace α]
[ConditionallyCompleteLinearOrder α]
[ClosedIciTopology α]
{f : γ → α}
[TopologicalSpace γ]
{S : Set γ}
(hS : Dense S)
(hf : Continuous f)
:
This is an analogue of Dense.continuous_inf for functions taking values in a conditionally
complete linear order. The assumption of BddBelow (range f) is not needed in this theorem.
theorem
ConditionallyCompleteLinearOrder.isCompact_Icc
{α : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
(a b : α)
:
A closed interval in a conditionally complete linear order is compact.
Also see general API on CompactIccSpace.
Existence of sequences tending to sInf or sSup of a given set #
theorem
IsLUB.exists_seq_strictMono_tendsto_of_notMem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{t : Set α}
{x : α}
[(nhds x).IsCountablyGenerated]
(htx : IsLUB t x)
(notMem : x ∉ t)
(ht : t.Nonempty)
:
∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
theorem
IsLUB.exists_seq_monotone_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{t : Set α}
{x : α}
[(nhds x).IsCountablyGenerated]
(htx : IsLUB t x)
(ht : t.Nonempty)
:
theorem
exists_seq_strictMono_tendsto'
{α : Type u_3}
[LinearOrder α]
[TopologicalSpace α]
[DenselyOrdered α]
[OrderTopology α]
[FirstCountableTopology α]
{x y : α}
(hy : y < x)
:
∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo y x) ∧ Filter.Tendsto u Filter.atTop (nhds x)
theorem
exists_seq_strictMono_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
[FirstCountableTopology α]
(x : α)
:
∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x)
theorem
exists_seq_strictMono_tendsto_nhdsWithin
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
[FirstCountableTopology α]
(x : α)
:
∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhdsWithin x (Set.Iio x))
theorem
exists_seq_tendsto_sSup
{α : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[FirstCountableTopology α]
{S : Set α}
(hS : S.Nonempty)
(hS' : BddAbove S)
:
∃ (u : ℕ → α), Monotone u ∧ Filter.Tendsto u Filter.atTop (nhds (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
theorem
Dense.exists_seq_strictMono_tendsto_of_lt
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[FirstCountableTopology α]
{s : Set α}
(hs : Dense s)
{x y : α}
(hy : y < x)
:
∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo y x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
theorem
Dense.exists_seq_strictMono_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMinOrder α]
[FirstCountableTopology α]
{s : Set α}
(hs : Dense s)
(x : α)
:
∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Iio x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
theorem
DenseRange.exists_seq_strictMono_tendsto_of_lt
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{β : Type u_3}
[LinearOrder β]
[DenselyOrdered α]
[FirstCountableTopology α]
{f : β → α}
{x y : α}
(hf : DenseRange f)
(hmono : Monotone f)
(hlt : y < x)
:
∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Ioo y x) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)
theorem
DenseRange.exists_seq_strictMono_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{β : Type u_3}
[LinearOrder β]
[DenselyOrdered α]
[NoMinOrder α]
[FirstCountableTopology α]
{f : β → α}
(hf : DenseRange f)
(hmono : Monotone f)
(x : α)
:
∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Iio x) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)
theorem
IsGLB.exists_seq_strictAnti_tendsto_of_notMem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{t : Set α}
{x : α}
[(nhds x).IsCountablyGenerated]
(htx : IsGLB t x)
(notMem : x ∉ t)
(ht : t.Nonempty)
:
∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
theorem
IsGLB.exists_seq_antitone_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{t : Set α}
{x : α}
[(nhds x).IsCountablyGenerated]
(htx : IsGLB t x)
(ht : t.Nonempty)
:
theorem
exists_seq_strictAnti_tendsto'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[FirstCountableTopology α]
{x y : α}
(hy : x < y)
:
∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo x y) ∧ Filter.Tendsto u Filter.atTop (nhds x)
theorem
exists_seq_strictAnti_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
[FirstCountableTopology α]
(x : α)
:
∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhds x)
theorem
exists_seq_strictAnti_tendsto_nhdsWithin
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
[FirstCountableTopology α]
(x : α)
:
∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhdsWithin x (Set.Ioi x))
theorem
exists_seq_strictAnti_strictMono_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[FirstCountableTopology α]
{x y : α}
(h : x < y)
:
∃ (u : ℕ → α) (v : ℕ → α),
StrictAnti u ∧ StrictMono v ∧ (∀ (k : ℕ), u k ∈ Set.Ioo x y) ∧ (∀ (l : ℕ), v l ∈ Set.Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ Filter.Tendsto v Filter.atTop (nhds y)
theorem
exists_seq_tendsto_sInf
{α : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[FirstCountableTopology α]
{S : Set α}
(hS : S.Nonempty)
(hS' : BddBelow S)
:
∃ (u : ℕ → α), Antitone u ∧ Filter.Tendsto u Filter.atTop (nhds (sInf S)) ∧ ∀ (n : ℕ), u n ∈ S
theorem
Dense.exists_seq_strictAnti_tendsto_of_lt
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[FirstCountableTopology α]
{s : Set α}
(hs : Dense s)
{x y : α}
(hy : x < y)
:
∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo x y ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
theorem
Dense.exists_seq_strictAnti_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
[DenselyOrdered α]
[NoMaxOrder α]
[FirstCountableTopology α]
{s : Set α}
(hs : Dense s)
(x : α)
:
∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioi x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
theorem
DenseRange.exists_seq_strictAnti_tendsto_of_lt
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{β : Type u_3}
[LinearOrder β]
[DenselyOrdered α]
[FirstCountableTopology α]
{f : β → α}
{x y : α}
(hf : DenseRange f)
(hmono : Monotone f)
(hlt : x < y)
:
∃ (u : ℕ → β), StrictAnti u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Ioo x y) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)
theorem
DenseRange.exists_seq_strictAnti_tendsto
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{β : Type u_3}
[LinearOrder β]
[DenselyOrdered α]
[NoMaxOrder α]
[FirstCountableTopology α]
{f : β → α}
(hf : DenseRange f)
(hmono : Monotone f)
(x : α)
:
∃ (u : ℕ → β), StrictAnti u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Ioi x) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)