restrict_eq_self_of_ae_mem — Mathlib

English

If a set s has μ-almost every point within it, then restricting μ to s yields μ itself.

Русский

Если μ-почти все точки принадлежат s, то ограничение μ на s равно μ.

LaTeX

$$$(\forallᵐ x \partial μ, x \in s) \implies μ.restrict s = μ$$$

Lean4

theorem restrict_eq_self_of_ae_mem {_m0 : MeasurableSpace α} ⦃s : Set α⦄ ⦃μ : Measure α⦄ (hs : ∀ᵐ x ∂μ, x ∈ s) :
    μ.restrict s = μ :=
  calc
    μ.restrict s = μ.restrict univ := restrict_congr_set (eventuallyEq_univ.mpr hs)
    _ = μ := restrict_univ

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