ofNNReal_liminf — Mathlib

English

For a sequence u: ι → NNReal, if f is CoboundedUnder (≥) by u, then the liminf of u in NNReal equals the liminf of its ENNReal embedding.

Русский

Для последовательности u: ι → NNReal, если fCoboundedUnder (≥) by u, то liminf в NNReal совпадает с liminf после вложения в ENNReal.

LaTeX

$$$$\\text{If } hf: f.\\text{IsCoboundedUnder}(\\ge)(u),\\quad \\liminf_{f} u = \\liminf_{f} (\\lambda i. (u(i) : \\mathbb{R}_{\\ge 0}^{\\infty})).$$$$

Lean4

@[simp, norm_cast]
theorem ofNNReal_liminf {u : ι → ℝ≥0} (hf : f.IsCoboundedUnder (· ≥ ·) u) :
    liminf u f = liminf (fun i ↦ (u i : ℝ≥0∞)) f :=
  by
  refine eq_of_forall_nnreal_iff fun r ↦ ?_
  rw [coe_le_coe, le_liminf_iff, le_liminf_iff]
  simp [forall_ennreal]

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