Documentation

Mathlib.Topology.Order.IsLUB

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) :
∃ᶠ (x : α) in nhds a, x s
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) :
∃ᶠ (x : α) in nhds a, x s
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_3} [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_3} [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)) :
IsLUB (f '' s) b
theorem IsGLB.mem_lowerBounds_of_tendsto {α : Type u_1} {γ : Type u_3} [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_3} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : MonotoneOn f s) :
IsGLB s as.NonemptyFilter.Tendsto f (nhdsWithin a s) (nhds b)IsGLB (f '' s) b
theorem IsLUB.mem_lowerBounds_of_tendsto {α : Type u_1} {γ : Type u_3} [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_3} [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)) :
IsGLB (f '' s) b
theorem IsGLB.mem_upperBounds_of_tendsto {α : Type u_1} {γ : Type u_3} [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_3} [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)) :
IsLUB (f '' s) 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 : xt) (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) :
∃ (u : α), Monotone u (∀ (n : ), u n x) Filter.Tendsto u Filter.atTop (nhds x) ∀ (n : ), u n t
theorem exists_seq_strictMono_tendsto' {α : Type u_4} [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_4} [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 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 : xt) (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) :
∃ (u : α), Antitone u (∀ (n : ), x u n) Filter.Tendsto u Filter.atTop (nhds x) ∀ (n : ), u n t
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_4} [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