English
If t is null-measurable with respect to μ, then for every subset s we have μ(s ∩ t) + μ(s \\ t) = μ(s).
Русский
Если t — нулево измеримое множество по отношении μ, тогда для любого множества s выполняется μ(s ∩ t) + μ(s \ t) = μ(s).
LaTeX
$$$\\forall s \\subseteq \\alpha,\\; \\text{NullMeasurableSet } t\\ μ:\\; \\mu(s \\cap t) + \\mu(s \\setminus t) = \\mu(s)$$$
Lean4
/-- A null measurable set `t` is Carathéodory measurable: for any `s`, we have
`μ (s ∩ t) + μ (s \ t) = μ s`. -/
theorem measure_inter_add_diff₀ (s : Set α) (ht : NullMeasurableSet t μ) : μ (s ∩ t) + μ (s \ t) = μ s :=
by
refine le_antisymm ?_ (measure_le_inter_add_diff _ _ _)
rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩
replace hs'm : NullMeasurableSet s' μ := hs'm.nullMeasurableSet
calc
μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) := by gcongr
_ = μ (s' ∩ t ∪ s' \ t) :=
(measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <| (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
_ = μ s' := (congr_arg μ (inter_union_diff _ _))
_ = μ s := hs'
