measure_toMeasurable_add_inter_right

English

Let s be measurable and (μ+ν)(t) ≠ ∞. Then ν(toMeasurable_{μ+ν}(t) ∩ s) = ν(t ∩ s).

Русский

Пусть s измеримо и (μ+ν)(t) ≠ ∞. Тогда ν(toMeasurable_{μ+ν}(t) ∩ s) = ν(t ∩ s).

LaTeX

$$$ (\\;s \\text{ MeasurableSet} \\;\\land\\ (μ+ν)(t) \\neq ∞\\ ) \\Rightarrow ν\\left( \\mathrm{toMeasurable}_{μ+ν}(t) \\cap s \\right) = ν\\left( t \\cap s \\right) $$$

Lean4

theorem measure_toMeasurable_add_inter_right {s t : Set α} (hs : MeasurableSet s) (ht : (μ + ν) t ≠ ∞) :
    ν (toMeasurable (μ + ν) t ∩ s) = ν (t ∩ s) :=
  by
  rw [add_comm] at ht ⊢
  exact measure_toMeasurable_add_inter_left hs ht

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