English
If u is measurable, v ⊆ w ⊆ u with w having zero s-measure, and 0 ≤[u] s, then s(v) = 0.
Русский
Пусть u, v, w — измеримые множества, v ⊆ w ⊆ u, и s допустимо неотрицательно на u, а s(w) = 0. Тогда s(v) = 0.
LaTeX
$$$$ (hi_1 : MeasurableSet i)\; (hv : MeasurableSet v)\; (hw : MeasurableSet w)\; (hsu : 0 \le_{u} s)\; (hw_1 : s w = 0)\; (hw_2 : w \subseteq u)\; (hwt : v \subseteq w) \;\Rightarrow\; s v = 0. $$$$
Lean4
/-- A subset `v` of a null-set `w` has zero measure if `w` is a subset of a positive set `u`. -/
theorem subset_positive_null_set (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : 0 ≤[u] s)
(hw₁ : s w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w) : s v = 0 :=
by
have : s v + s (w \ v) = 0 := by
rw [← hw₁, ← of_union Set.disjoint_sdiff_right hv (hw.diff hv), Set.union_diff_self,
Set.union_eq_self_of_subset_left hwt]
have h₁ := nonneg_of_zero_le_restrict _ (restrict_le_restrict_subset _ _ hu hsu (hwt.trans hw₂))
have h₂ : 0 ≤ s (w \ v) :=
nonneg_of_zero_le_restrict _ (restrict_le_restrict_subset _ _ hu hsu (diff_subset.trans hw₂))
linarith
