ae_restrict_iff' — Mathlib

English

Let hs be NullMeasurableSet s μ. Then (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x.

Русский

Пусть hs: NullMeasurableSet s μ. Тогда (∀ почти все x ∈ s, p x) эквивалентно (∀ почти все x, x ∈ s ⇒ p x).

LaTeX

$$$\text{NullMeasurableSet}(s, μ) \Rightarrow (\forall^\mathrm{a.e.}_{x} p(x) \text{ w.r.t. } μ|_s) \iff (\forall^\mathrm{a.e.}_{x} [x \in s \to p(x)] \text{ w.r.t. } μ).$$$

Lean4

theorem ae_restrict_iff' {p : α → Prop} (hs : MeasurableSet s) : (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x :=
  ae_restrict_iff'₀ hs.nullMeasurableSet

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