measureReal_iUnion_fintype_le — Mathlib

English

For a finite index type, the real measure of the union over all indices is at most the sum over those indices.

Русский

Для конечного индекса μ.real(⋃_{b} f(b)) ≤ ∑_{b} μ.real(f(b)).

LaTeX

$$$ \\mu.real (\\bigcup_{b} f(b)) \\leq \\sum_{p} \\mu.real (f(p)) $$$

Lean4

theorem measureReal_iUnion_fintype_le [Fintype β] (f : β → Set α) : μ.real (⋃ b, f b) ≤ ∑ p, μ.real (f p) :=
  by
  convert measureReal_biUnion_finset_le Finset.univ f
  simp

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