instMeasurableAdd₂ — Mathlib

English

The addition of two measures defines a measurable addition operation on the space of measures; i.e., Measure α is closed under measurable addition.

Русский

Сложение двух мер задаёт измеримое сложение на пространстве мер; Measure α замкнуто относительно измеримого сложения.

LaTeX

$$$\text{MeasurableAdd₂}(\text{Measure }\alpha)$$$

Lean4

instance instMeasurableAdd₂ {α : Type*} {m : MeasurableSpace α} : MeasurableAdd₂ (Measure α) :=
  by
  refine ⟨Measure.measurable_of_measurable_coe _ fun s hs => ?_⟩
  simp_rw [Measure.coe_add, Pi.add_apply]
  refine Measurable.add ?_ ?_
  · exact (Measure.measurable_coe hs).comp measurable_fst
  · exact (Measure.measurable_coe hs).comp measurable_snd

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