iSup_eq_of_forall_le_of_tendsto — Mathlib

English

If ∀ i, f(i) ≤ a and Tendsto f F (nhds a), then ⨆ i, f(i) = a.

Русский

Если ∀ i, f(i) ≤ a и Tendsto f F (nhds a), тогда ⨆ i, f(i) = a.

LaTeX

$$⨆ i, f i = a$$

Lean4

theorem iSup_eq_of_forall_le_of_tendsto {ι : Type*} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLattice α]
    [TopologicalSpace α] [ClosedIicTopology α] {a : α} {f : ι → α} (hle : ∀ i, f i ≤ a)
    (hlim : Filter.Tendsto f F (𝓝 a)) : ⨆ i, f i = a :=
  have := F.nonempty_of_neBot
  (IsLUB.range_of_tendsto hle hlim).ciSup_eq

Похожие утверждения