add_measure_right — Mathlib

English

Extends FinMeasAdditive to finite unions of disjoint sets indexed by a finite index set.

Русский

Расширение FinMeasAdditive к конечным объединениям непересекающихся множеств с индексами во множества ι.

LaTeX

$$map_iUnion_fin_meas_set_eq_sum …$$

Lean4

theorem add_measure_right {_ : MeasurableSpace α} (μ ν : Measure α) (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) :
    DominatedFinMeasAdditive (μ + ν) T C :=
  of_measure_le (Measure.le_add_right le_rfl) hT hC

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