English
For a sequence u: ι → NNReal, if f is bounded under ≤ by u, then the limsup taken in NNReal equals the limsup of the image of u into ENNReal (i.e., after embedding NNReal into ENNReal).
Русский
Для последовательности u: ι → NNReal, если f ограничено по отношению к u сверху, то limsup в NNReal совпадает с limsup после вложения u в ENNReal.
LaTeX
$$$$\\text{If } hf: f.\\text{IsBoundedUnder}(\\le)(u),\\quad \\limsup_{f} u = \\limsup_{f} (\\lambda i. (u(i) : \\mathbb{R}_{\\ge 0}^{\\infty})).$$$$
Lean4
@[simp, norm_cast]
theorem ofNNReal_limsup {u : ι → ℝ≥0} (hf : f.IsBoundedUnder (· ≤ ·) u) :
limsup u f = limsup (fun i ↦ (u i : ℝ≥0∞)) f :=
by
refine eq_of_forall_nnreal_iff fun r ↦ ?_
rw [coe_le_coe, le_limsup_iff, le_limsup_iff]
simp [forall_ennreal]
