measure_toMeasurable_add_inter_left

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_left {s t : Set α} (hs : MeasurableSet s) (ht : (μ + ν) t ≠ ∞) :
    μ (toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s) :=
  by
  refine (measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm
  · refine measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _) (measure_toMeasurable t).symm
    rwa [measure_toMeasurable t]
  · simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at ht
    exact ht.1

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