add_measure_left — Mathlib

English

If hT is dominated FinMeasAdditive for ν, then μ+ν remains dominated FinMeasAdditive.

Русский

Если hT доминированная FinMeasAdditive для ν, тогда μ+ν остаётся доминированной FinMeasAdditive.

LaTeX

$$add_measure_left μ ν hT hC$$

Lean4

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

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