English
For any f: α → ENNReal, any n, a, eapprox f n a is always strictly less than ∞.
Русский
Для любого f: α → ENNReal, любого n, любого a, eapprox f n a < ∞.
LaTeX
$$$ eapprox\_lt\_top\ (f\ a) \ n \ a : eapprox f n a < \infty $$$
Lean4
theorem eapprox_lt_top (f : α → ℝ≥0∞) (n : ℕ) (a : α) : eapprox f n a < ∞ :=
by
simp only [eapprox, approx, finset_sup_apply, restrict]
rw [Finset.sup_lt_iff (α := ℝ≥0∞) WithTop.top_pos]
intro b _
split_ifs
· simp only [coe_zero, coe_piecewise, piecewise_eq_indicator, coe_const]
calc
{a : α | ennrealRatEmbed b ≤ f a}.indicator (fun _ => ennrealRatEmbed b) a ≤ ennrealRatEmbed b :=
indicator_le_self _ _ a
_ < ⊤ := ENNReal.coe_lt_top
· exact WithTop.top_pos