Properties of LUB and GLB in an order topology #

theorem IsLUB.frequently_mem {α : Type u_1} [] [] [] {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} [] [] [] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) :
∃ᶠ (x : α) in nhds a, x s
theorem IsGLB.frequently_mem {α : Type u_1} [] [] [] {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} [] [] [] {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) :
∃ᶠ (x : α) in nhds a, x s
theorem IsLUB.mem_closure {α : Type u_1} [] [] [] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) :
a
theorem IsGLB.mem_closure {α : Type u_1} [] [] [] {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) :
a
theorem IsLUB.nhdsWithin_neBot {α : Type u_1} [] [] [] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) :
(nhdsWithin a s).NeBot
theorem IsGLB.nhdsWithin_neBot {α : Type u_1} [] [] [] {a : α} {s : Set α} :
IsGLB s as.Nonempty(nhdsWithin a s).NeBot
theorem isLUB_of_mem_nhds {α : Type u_1} [] [] [] {s : Set α} {a : α} {f : } (hsa : a ) (hsf : s f) [(f nhds a).NeBot] :
IsLUB s a
theorem isLUB_of_mem_closure {α : Type u_1} [] [] [] {s : Set α} {a : α} (hsa : a ) (hsf : a ) :
IsLUB s a
theorem isGLB_of_mem_nhds {α : Type u_1} [] [] [] {s : Set α} {a : α} {f : } :
a s f(f nhds a).NeBotIsGLB s a
theorem isGLB_of_mem_closure {α : Type u_1} [] [] [] {s : Set α} {a : α} (hsa : a ) (hsf : a ) :
IsGLB s a
theorem IsLUB.mem_upperBounds_of_tendsto {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : ) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
theorem IsLUB.isLUB_of_tendsto {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : ) (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} [] [] [] [] [] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : ) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
theorem IsGLB.isGLB_of_tendsto {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : ) :
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} [] [] [] [] [] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : ) (ha : IsLUB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
theorem IsLUB.isGLB_of_tendsto {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} {s : Set α} {a : α} {b : γ} :
IsLUB s as.NonemptyFilter.Tendsto f (nhdsWithin a s) (nhds b)IsGLB (f '' s) b
theorem IsGLB.mem_upperBounds_of_tendsto {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} {s : Set α} {a : α} {b : γ} (hf : ) (ha : IsGLB s a) (hb : Filter.Tendsto f (nhdsWithin a s) (nhds b)) :
theorem IsGLB.isLUB_of_tendsto {α : Type u_1} {γ : Type u_3} [] [] [] [] [] {f : αγ} {s : Set α} {a : α} {b : γ} :
IsGLB s as.NonemptyFilter.Tendsto f (nhdsWithin a s) (nhds b)IsLUB (f '' s) b
theorem IsLUB.mem_of_isClosed {α : Type u_1} [] [] [] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) (sc : ) :
a s
theorem IsClosed.isLUB_mem {α : Type u_1} [] [] [] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) (sc : ) :
a s

Alias of IsLUB.mem_of_isClosed.

theorem IsGLB.mem_of_isClosed {α : Type u_1} [] [] [] {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) (sc : ) :
a s
theorem IsClosed.isGLB_mem {α : Type u_1} [] [] [] {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) (sc : ) :
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} [] [] [] {t : Set α} {x : α} [(nhds x).IsCountablyGenerated] (htx : IsLUB t x) (not_mem : xt) (ht : t.Nonempty) :
∃ (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} [] [] [] {t : Set α} {x : α} [(nhds x).IsCountablyGenerated] (htx : IsLUB t x) (ht : t.Nonempty) :
∃ (u : α), (∀ (n : ), u n x) Filter.Tendsto u Filter.atTop (nhds x) ∀ (n : ), u n t
theorem exists_seq_strictMono_tendsto' {α : Type u_4} [] [] [] [] {x : α} {y : α} (hy : y < x) :
∃ (u : α), (∀ (n : ), u n Set.Ioo y x) Filter.Tendsto u Filter.atTop (nhds x)
theorem exists_seq_strictMono_tendsto {α : Type u_1} [] [] [] [] [] (x : α) :
∃ (u : α), (∀ (n : ), u n < x) Filter.Tendsto u Filter.atTop (nhds x)
theorem exists_seq_strictMono_tendsto_nhdsWithin {α : Type u_1} [] [] [] [] [] (x : α) :
∃ (u : α), (∀ (n : ), u n < x) Filter.Tendsto u Filter.atTop (nhdsWithin x (Set.Iio x))
theorem exists_seq_tendsto_sSup {α : Type u_4} [] [] {S : Set α} (hS : S.Nonempty) (hS' : ) :
∃ (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} [] [] [] {t : Set α} {x : α} [(nhds x).IsCountablyGenerated] (htx : IsGLB t x) (not_mem : xt) (ht : t.Nonempty) :
∃ (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} [] [] [] {t : Set α} {x : α} [(nhds x).IsCountablyGenerated] (htx : IsGLB t x) (ht : t.Nonempty) :
∃ (u : α), (∀ (n : ), x u n) Filter.Tendsto u Filter.atTop (nhds x) ∀ (n : ), u n t
theorem exists_seq_strictAnti_tendsto' {α : Type u_1} [] [] [] [] {x : α} {y : α} (hy : x < y) :
∃ (u : α), (∀ (n : ), u n Set.Ioo x y) Filter.Tendsto u Filter.atTop (nhds x)
theorem exists_seq_strictAnti_tendsto {α : Type u_1} [] [] [] [] [] (x : α) :
∃ (u : α), (∀ (n : ), x < u n) Filter.Tendsto u Filter.atTop (nhds x)
theorem exists_seq_strictAnti_tendsto_nhdsWithin {α : Type u_1} [] [] [] [] [] (x : α) :
∃ (u : α), (∀ (n : ), x < u n) Filter.Tendsto u Filter.atTop (nhdsWithin x (Set.Ioi x))
theorem exists_seq_strictAnti_strictMono_tendsto {α : Type u_1} [] [] [] [] {x : α} {y : α} (h : x < y) :
∃ (u : α) (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} [] [] {S : Set α} (hS : S.Nonempty) (hS' : ) :
∃ (u : α), Filter.Tendsto u Filter.atTop (nhds (sInf S)) ∀ (n : ), u n S