unifIntegrable_zero_meas — Mathlib

English

Any family of functions is uniformly integrable with respect to the zero measure, for any p and index set.

Русский

Любое семейство функций является Uniform Integrable по отношению к нулевой мере.

LaTeX

$$$\\operatorname{UnifIntegrable} f p (0: Measure α)$$$

Lean4

theorem unifIntegrable_zero_meas [MeasurableSpace α] {p : ℝ≥0∞} {f : ι → α → β} : UnifIntegrable f p (0 : Measure α) :=
  fun ε _ => ⟨1, one_pos, fun i s _ _ => by simp⟩

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