English
The limit inferior commutes with the real coercion: taking liminf of a Real-valued sequence obtained from NNReal values equals the liminf of the NNReal sequence viewed in Real.
Русский
Предел нижнего значения сочетает предел с приведением к действительным: лиминф последовательности в Real совпадает с лимinf последовательности NNReal после приведения к Real.
LaTeX
$$$\\\\liminf_f ((u(i))^{\\\\mathbb{R}}) = (\\\\liminf_f u(i))^{\\\\mathbb{R}}$$$
Lean4
@[simp, norm_cast]
theorem toReal_liminf : liminf (fun i ↦ (u i : ℝ)) f = liminf u f :=
by
by_cases hf : f.IsCoboundedUnder (· ≥ ·) u; swap
· simp [*]
refine eq_of_forall_le_iff fun c ↦ ?_
rw [← Real.toNNReal_le_iff_le_coe, le_liminf_iff (by simpa) ⟨0, by simp⟩, le_liminf_iff]
simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt, zero_le_coe,
IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_swap (α := _ ≤ _)]
refine forall₂_congr fun r hr ↦ ?_
simpa using (le_or_gt 0 r).imp_right fun hr ↦ .of_forall fun i ↦ hr.trans_le (by simp)
