sub_apply_eq_zero_of_isHahnDecomposition

English

If IsHahnDecomposition μ ν s holds, then (μ - ν)(s) = 0.

Русский

Если выполняется IsHahnDecomposition μ ν s, то (μ - ν)(s) = 0.

LaTeX

$$$$ IsHahnDecomposition(μ, ν, s) \Rightarrow (μ - ν)(s) = 0. $$$$

Lean4

theorem sub_apply_eq_zero_of_isHahnDecomposition (hs : IsHahnDecomposition μ ν s) : (μ - ν) s = 0 :=
  by
  rw [← restrict_eq_zero, restrict_sub_eq_restrict_sub_restrict hs.measurableSet]
  exact sub_eq_zero_of_le hs.le_on

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