add_measure — Mathlib

English

If f preserves μa→μb and μa'→μb' as measures, then f preserves the sum μa+μa' to μb+μb'.

Русский

Если f сохраняет μa→μb и μa'→μb', то сохраняет сумму мер μa+μa' в μb+μb'.

LaTeX

$$$\text{MeasurePreserving } f\, μ_a\, μ_b \rightarrow \text{MeasurePreserving } f\, μ_{a'}\, μ_{b'} \rightarrow \text{MeasurePreserving } f\, (μ_a+μ_{a'})\, (μ_b+μ_{b'})$$$

Lean4

theorem add_measure {f μa' μb'} (hf : MeasurePreserving f μa μb) (hf' : MeasurePreserving f μa' μb') :
    MeasurePreserving f (μa + μa') (μb + μb')
    where
  measurable := hf.measurable
  map_eq := by rw [Measure.map_add _ _ hf.measurable, hf.map_eq, hf'.map_eq]

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