ae_eq_of_subset_of_measure_ge — Mathlib

English

If s ⊆ t and μ t ≤ μ s, with μ s finite and s null-measurable, then μ(s Δ t) = 0, i.e., s =ᵐ t.

Русский

Если s ⊆ t и μ t ≤ μ s, причём μ s конечна и s нулево измеримо, то μ (симметрический разность) равно нулю, то есть s =ᵐ t.

LaTeX

$$$ (s \subseteq t) \rightarrow (μ t ≤ μ s) \rightarrow (NullMeasurableSet(s, μ)) \rightarrow (μ t \,\neq\, ∞) \rightarrow (s =^{\mu}_{\mathrm{a.e.}} t) $$$

Lean4

/-- If `s ⊆ t`, `μ t ≤ μ s`, `μ t ≠ ∞`, and `s` is measurable, then `s =ᵐ[μ] t`. -/
theorem ae_eq_of_subset_of_measure_ge (h₁ : s ⊆ t) (h₂ : μ t ≤ μ s) (hsm : NullMeasurableSet s μ) (ht : μ t ≠ ∞) :
    s =ᵐ[μ] t :=
  ae_eq_of_ae_subset_of_measure_ge (HasSubset.Subset.eventuallyLE h₁) h₂ hsm ht

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