sub_apply_eq_zero_of_restrict_le_restrict

English

If μ.restrict s ≤ ν.restrict s, then (μ − ν) s = 0 for measurable s.

Русский

Если μ.restrict s ≤ ν.restrict s, тогда (μ − ν) s = 0 для измеримого s.

LaTeX

$$$[μ.restrict s \\le ν.restrict s] \\\\Rightarrow (\\\\mu - \\\\nu) \\\\ s = 0 \\\\text{, when } s \\\\text{ measurable}$$$

Lean4

theorem sub_apply_eq_zero_of_restrict_le_restrict (h_le : μ.restrict s ≤ ν.restrict s) (h_meas_s : MeasurableSet s) :
    (μ - ν) s = 0 := by
  rw [← restrict_apply_self, restrict_sub_eq_restrict_sub_restrict, sub_eq_zero_of_le] <;> simp [*]

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