iInf_eq_of_forall_le_of_tendsto — Mathlib

English

The infimum over i of f i equals a when each f i ≥ a and f tends to a.

Русский

Если для всех i выполняется a ≤ f i и f стремится к a, то iInf_i f i = a.

LaTeX

$$$ (\forall i, a \le f i) \rightarrow Tendsto f F (nhds a) \rightarrow iInf (\lambda i, f i) = a $$$

Lean4

theorem iInf_eq_of_forall_le_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLattice α]
    [TopologicalSpace α] [ClosedIciTopology α] {a : α} {f : ι → α} (hle : ∀ i, a ≤ f i) (hlim : Tendsto f F (𝓝 a)) :
    ⨅ i, f i = a :=
  iSup_eq_of_forall_le_of_tendsto (α := αᵒᵈ) hle hlim

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