all_ae_ofReal_F_le_bound — Mathlib

English

If Tendsto F' n a → f' a almost everywhere, then Tendsto ENNReal.ofReal ‖F' n a‖ → ENNReal.ofReal ‖f' a‖ in the same sense almost everywhere.

Русский

Если для почти всех a верно Tendsto F' n a → f' a, то аналогично верно Tendsto ENNReal.ofReal ‖F' n a‖ → ENNReal.ofReal ‖f' a‖ почти всюду.

LaTeX

$$$\forallᵃᵉ a, Tendsto (f) (atTop) (nhds f') \Rightarrow Tendsto (‖f‖) (atTop) (nhds ‖f'‖)$$$

Lean4

theorem all_ae_ofReal_F_le_bound (h : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a) :
    ∀ n, ∀ᵐ a ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a) := fun n =>
  (h n).mono fun _ h => ENNReal.ofReal_le_ofReal h

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