measure_diff_le_iff_le_add — Mathlib

English

For s ⊆ t with μ(s) ≠ ∞, μ(t \\ s) ≤ ε iff μ(t) ≤ μ(s) + ε.

Русский

Для s ⊆ t с μ(s) ≠ ∞ верно: μ(t \\ s) ≤ ε ⇔ μ(t) ≤ μ(s) + ε.

LaTeX

$$$$ \\mu(t \\setminus s) \\le \\varepsilon \\iff \\mu(t) \\le \\mu(s) + \\varepsilon. $$$$

Lean4

theorem measure_diff_le_iff_le_add (hs : NullMeasurableSet s μ) (hst : s ⊆ t) (hs' : μ s ≠ ∞) {ε : ℝ≥0∞} :
    μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε := by rw [measure_diff hst hs hs', tsub_le_iff_left]

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