abs_measureReal_sub_le_measureReal_symmDiff

English

For finite μ and null-measurable s, t, we have |μ.real s − μ.real t| ≤ μ.real (s Δ t).

Русский

Для конечной μ и нуль-измеримых s, t верно: |μ.real(s) − μ.real(t)| ≤ μ.real(s Δ t).

LaTeX

$$$\text{IsFiniteMeasure}(\mu) \Rightarrow |\mu.real s - \mu.real t| \le \mu.real (s \Delta t)$$$

Lean4

theorem abs_measureReal_sub_le_measureReal_symmDiff [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ)
    (ht : NullMeasurableSet t μ) : |μ.real s - μ.real t| ≤ μ.real (s ∆ t) :=
  abs_measureReal_sub_le_measureReal_symmDiff' hs ht (measure_ne_top μ s) (measure_ne_top μ t)

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