measure_union_toMeasurable — Mathlib

English

The measure of the union with toMeasurable on one side equals the measure of the plain union: μ(s ∪ toMeasurable μ t) = μ(s ∪ t).

Русский

Мера объединения с toMeasurable по одной стороне равна мере обычного объединения: μ(s ∪ toMeasurable μ t) = μ(s ∪ t).

LaTeX

$$$ μ\bigl(s \cup toMeasurable μ t\bigr) = μ\bigl(s \cup t\bigr) $$$

Lean4

@[simp]
theorem measure_union_toMeasurable : μ (s ∪ toMeasurable μ t) = μ (s ∪ t) :=
  Eq.symm <| measure_union_congr_of_subset Subset.rfl le_rfl (subset_toMeasurable _ _) (measure_toMeasurable _).le

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