aeSeq — Mathlib

English

If a.e. equality holds for all measurable sets s, then f and g are a.e.-equal.

Русский

Если a.e. равенство верно для всех измеримых множеств s, то f и g равны почти повсюду.

LaTeX

$$$$ f =^{\mathrm{ae}}_{\mu} g $$$$

Lean4

/-- A sequence of measurable functions that are equal to `f` and verify property `p` on the
measurable set `aeSeqSet hf p`. -/
noncomputable def aeSeq (hf : ∀ i, AEMeasurable (f i) μ) (p : α → (ι → β) → Prop) : ι → α → β := fun i x =>
  ite (x ∈ aeSeqSet hf p) ((hf i).mk (f i) x) (⟨f i x⟩ : Nonempty β).some

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