English
If the liminf of the Real nnabs of x_n is finite, then there exists R such that Frequent (x_n < R) holds under ENNReal context, with a Real-valued axiom.
Русский
Если лиминфим nnabs(x_n) конечен, существует R, такой что x_n < R встречается часто (в контексте Real), что соответствует эннереал.
LaTeX
$$$\\text{liminf}_{l} (|x_n|) \\\\neq \\infty \\Rightarrow \\exists R, \\text{Frequently}_{l}(x_n < R).$$$
Lean4
theorem exists_frequently_lt_of_liminf_ne_top' {ι : Type*} {l : Filter ι} {x : ι → ℝ}
(hx : liminf (fun n => (Real.nnabs (x n) : ℝ≥0∞)) l ≠ ∞) : ∃ R, ∃ᶠ n in l, R < x n :=
by
by_contra h
simp_rw [not_exists, not_frequently, not_lt] at h
refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)
simp only [eventually_map, ENNReal.coe_le_coe]
filter_upwards [h (-r)] with i hi using (le_neg.1 hi).trans (neg_le_abs _)
