English
If w ⊆ u and s ≤[u] 0, and s(w) = 0, then any subset v ⊆ w also has s(v) = 0 (the analogous statement to the positive-null set lemma under negation).
Русский
Если w ⊆ u и s ≤[u] 0, а s(w) = 0, то любая подподмножество v ⊆ w также имеет s(v) = 0 (аналогично лемме о нуле на положительной части, но для отрицательной части).
LaTeX
$$$$ (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : s ≤[u] 0) (hw_1 : s w = 0) (hw_2 : w \subseteq u) (hwt : v \subseteq w) : s v = 0. $$$$
Lean4
/-- A subset `v` of a null-set `w` has zero measure if `w` is a subset of a negative set `u`. -/
theorem subset_negative_null_set (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : s ≤[u] 0)
(hw₁ : s w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w) : s v = 0 :=
by
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu
have := subset_positive_null_set hu hv hw hsu
simp only [Pi.neg_apply, neg_eq_zero, coe_neg] at this
exact this hw₁ hw₂ hwt
