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)
:
∃ᶠ (x : α) in nhdsWithin a (Set.Iic a), x ∈ s
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)
:
∃ᶠ (x : α) in nhdsWithin a (Set.Ici a), x ∈ s
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))
:
b ∈ upperBounds (f '' s)
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))
:
b ∈ lowerBounds (f '' s)
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))
:
b ∈ lowerBounds (f '' s)
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))
:
b ∈ upperBounds (f '' s)
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)
:
a ∈ s
theorem
IsClosed.isLUB_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsLUB s a)
(hs : s.Nonempty)
(sc : IsClosed s)
:
a ∈ 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)
:
a ∈ s
theorem
IsClosed.isGLB_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{a : α}
{s : Set α}
(ha : IsGLB s a)
(hs : s.Nonempty)
(sc : IsClosed s)
:
a ∈ s
Alias of IsGLB.mem_of_isClosed.
Existence of sequences tending to sInf or sSup of a given set #
theorem
IsLUB.exists_seq_strictMono_tendsto_of_not_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{t : Set α}
{x : α}
[(nhds x).IsCountablyGenerated]
(htx : IsLUB t x)
(not_mem : x ∉ t)
(ht : t.Nonempty)
:
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)
:
theorem
IsGLB.exists_seq_strictAnti_tendsto_of_not_mem
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{t : Set α}
{x : α}
[(nhds x).IsCountablyGenerated]
(htx : IsGLB t x)
(not_mem : x ∉ t)
(ht : t.Nonempty)
:
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)
:
theorem
exists_seq_tendsto_sInf
{α : Type u_3}
[ConditionallyCompleteLinearOrder α]
[TopologicalSpace α]
[OrderTopology α]
[FirstCountableTopology α]
{S : Set α}
(hS : S.Nonempty)
(hS' : BddBelow S)
: