measure_diff_lt_of_lt_add — Mathlib

English

If s is null-measurable, s ⊆ t, μ(s) ≠ ∞, then for every ε, μ(t) < μ(s) + ε ⇒ μ(t \\ s) < ε.

Русский

Если s нулемеримо измеримо, s ⊆ t, μ(s) ≠ ∞, тогда для всякого ε: μ(t) < μ(s) + ε ⇒ μ(t \\ s) < ε.

LaTeX

$$$$ \\forall \\varepsilon \\; ( \\mu t < \\mu s + \\varepsilon ) \\Rightarrow \\mu(t \\setminus s) < \\varepsilon, $$ с условиями: hs, hst, hs'.$$

Lean4

theorem measure_diff_lt_of_lt_add (hs : NullMeasurableSet s μ) (hst : s ⊆ t) (hs' : μ s ≠ ∞) {ε : ℝ≥0∞}
    (h : μ t < μ s + ε) : μ (t \ s) < ε := by
  rw [measure_diff hst hs hs']; rw [add_comm] at h
  exact ENNReal.sub_lt_of_lt_add (measure_mono hst) h

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