English
The assignment that sends a continuous map f: α → β to its equivalence class of μ-a.e. measurable representatives, f.toAEEqFun μ, is a well-defined map from ContinuousMap α β to the AEEqFun α β μ space.
Русский
Отображение, отправляющее непрерывную карту f: α → β в её эквивалентность по μ почти везде измеримых представителей, f.toAEEqFun μ, является корректным отображением из ContinuousMap α β в пространство AEEqFun α β μ.
LaTeX
$$$f \mapsto \mathrm{AEEqFun}(f, \mu) \quad : \; C(\alpha, \beta) \to \alpha \to_{μ} \beta$$$
Lean4
/-- The equivalence class of `μ`-almost-everywhere measurable functions associated to a continuous
map. -/
def toAEEqFun (f : C(α, β)) : α →ₘ[μ] β :=
AEEqFun.mk f f.continuous.aestronglyMeasurable
