iSup₂_lintegral_le — Mathlib

English

For a two-parameter family f_i_j, the double supremum of the integrals is bounded by the integral of the pointwise double supremum.

Русский

Для двойного семейства f_i_j супремум интегралов не превышает интеграл по точечному двойному супремуму.

LaTeX

$$$$ \sup_i\sup_j \int^- a, f_i_j(a) \partial \mu \le \int^- a, \sup_i\sup_j f_i_j(a) \partial \mu. $$$$

Lean4

theorem iSup₂_lintegral_le {ι : Sort*} {ι' : ι → Sort*} (f : ∀ i, ι' i → α → ℝ≥0∞) :
    ⨆ (i) (j), ∫⁻ a, f i j a ∂μ ≤ ∫⁻ a, ⨆ (i) (j), f i j a ∂μ :=
  by
  convert (monotone_lintegral μ).le_map_iSup₂ f with a
  simp only [iSup_apply]

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