liminf_top_eq_ciInf — Mathlib

English

If range u is bounded below and β is nonempty, then liminf u ⊤ equals the infimum of the values u(i).

Русский

Если диапазон u ограничен снизу и множество β непусто, то liminf u вверху равен наименьшему элементу {u(i)}.

LaTeX

$$$ \\operatorname{liminf} u \\top = \\bigwedge_{i} u(i) $$$

Lean4

theorem liminf_top_eq_ciInf [Nonempty β] (hu : BddBelow (range u)) : liminf u ⊤ = ⨅ i, u i := by
  rw [liminf, map_top, limsInf_principal_eq_csSup hu (range_nonempty _), sInf_range]

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