measure_mono_ae — Mathlib

English

If s ≤ᵐ[μ] t, then μ s ≤ μ t.

Русский

Если s меньше или равно t почти по μ, то μ s ≤ μ t.

LaTeX

$$$\forall s,t\subseteq\alpha,\; s \leq_{\mathrm{ae}}^{\mu} t \Rightarrow \mu s \le \mu t$$$

Lean4

/-- If `s ⊆ t` modulo a set of measure `0`, then `μ s ≤ μ t`. -/
@[mono]
theorem measure_mono_ae (H : s ≤ᵐ[μ] t) : μ s ≤ μ t :=
  calc
    μ s ≤ μ (s ∪ t) := measure_mono subset_union_left
    _ = μ (t ∪ s \ t) := by rw [union_diff_self, Set.union_comm]
    _ ≤ μ t + μ (s \ t) := (measure_union_le _ _)
    _ = μ t := by rw [ae_le_set.1 H, add_zero]

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