inv_liminf — Mathlib

English

For any index set ι, any family x : ι → ℝ≥0∞ and any filter l on ι, the inverse of liminf equals limsup of inverses: (liminf x l)⁻¹ = limsup (i ↦ (x i)⁻¹) l.

Русский

Для любых индексов ι, семейство x: ι → ℝ≥0∞ и фильтр l на ι, обратное к liminf равно limsup обратных значений: (liminf x l)⁻¹ = limsup (i ↦ (x i)⁻¹) l.

LaTeX

$$$(\\liminf_{i} x_i)^{-1} = \\limsup_{i} (x_i)^{-1}.$$$

Lean4

theorem inv_liminf {ι : Sort _} {x : ι → ℝ≥0∞} {l : Filter ι} : (liminf x l)⁻¹ = limsup (fun i => (x i)⁻¹) l :=
  OrderIso.invENNReal.liminf_apply

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