eapprox_lt_top — Mathlib

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

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