inv_limsup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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