English
Let m be an outer measure on α and h a Carathéodory bound such that ms ≤ m.caratheodory. If s is NullMeasurable with respect to m.toMeasure h, then the measure m.toMeasure h assigns to s equals the outer measure m assigns to s: m.toMeasure h s = m s.
Русский
Пусть m — внешняя мера на α и h удовлетворяет условию Карatheodory с ms ≤ m.caratheodory. Если s является NullMeasurable относительно m.toMeasure h, то мера m.toMeasure h присваивает s ту же величину, что и m: m.toMeasure h s = m s.
LaTeX
$$$\\forall m:\\, \\text{OuterMeasure }\\alpha,\\ \\forall h:\\ ms \\le m.caratheodory,\\ \\forall s:\\ Set\\,\\alpha,\\ \\text{NullMeasurableSet } s (m.toMeasure h) \\ \\Rightarrow\\ m.toMeasure h\\,s = m\\,s.$$$
Lean4
theorem toMeasure_apply₀ (m : OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α}
(hs : NullMeasurableSet s (m.toMeasure h)) : m.toMeasure h s = m s :=
by
refine le_antisymm ?_ (le_toMeasure_apply _ _ _)
rcases hs.exists_measurable_subset_ae_eq with ⟨t, hts, htm, heq⟩
calc
m.toMeasure h s = m.toMeasure h t := measure_congr heq.symm
_ = m t := (toMeasure_apply m h htm)
_ ≤ m s := m.mono hts
