measure_union₀_aux — Mathlib

English

Let s and t be null-measurable sets with respect to μ and be almost everywhere disjoint; then μ(s ∪ t) = μ(s) + μ(t).

Русский

Пусть s и t — множества, нулево измеримые относительно μ, и они почти не пересекаются; тогда μ(s ∪ t) = μ(s) + μ(t).

LaTeX

$$$\mathrm{NullMeasurableSet}(s,\mu) \land \mathrm{NullMeasurableSet}(t,\mu) \land \mathrm{AEDisjoint}(\mu, s, t) \Rightarrow \mu(s \cup t) = \mu(s) + \mu(t).$$$

Lean4

theorem measure_union₀_aux (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (hd : AEDisjoint μ s t) :
    μ (s ∪ t) = μ s + μ t :=
  by
  rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond]
  exacts [(pairwise_on_bool AEDisjoint.symmetric).2 hd, fun b => Bool.casesOn b ht hs]

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