measure_union_add_inter₀' — Mathlib

English

If s is null-measurable and s is almost disjoint from t, then μ(s ∪ t) = μ(s) + μ(t).

Русский

Если s нулево измеримо и почти не пересекается с t, то μ( s ∪ t ) = μ(s) + μ(t).

LaTeX

$$$\mathrm{NullMeasurableSet}(s,\mu) \Rightarrow \forall t,\; \mu(s \cup t) = \mu(s) + \mu(t) - \mu(s \cap t).$$$

Lean4

theorem measure_union_add_inter₀' (hs : NullMeasurableSet s μ) (t : Set α) : μ (s ∪ t) + μ (s ∩ t) = μ s + μ t := by
  rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]

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