AEEqFun — Mathlib

English

Coercion from AEEqFun to functions is given by a canonical cast that realizes the representative function on the underlying space.

Русский

Коэрцирование AEEqFun к функциям реализуется через каноническое приведение к представленной функции на базовом пространстве.

LaTeX

$$def cast (f : α →ₘ[μ] β) : α → β$$

Lean4

/-- The space of equivalence classes of almost everywhere strongly measurable functions, where two
strongly measurable functions are equivalent if they agree almost everywhere, i.e.,
they differ on a set of measure `0`. -/
def AEEqFun (μ : Measure α) : Type _ :=
  Quotient (μ.aeEqSetoid β)

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