mk — Mathlib · SciLib

English

The map mk corresponds to forming the representative class; mk is compatible with the quotient construction.

Русский

Карта mk образует представительный класс; mk совместима с конструкцией квартизирования.

LaTeX

$$mk {α} hf : (α → β) → MeasureTheory.AEEqFun α β μ$$

Lean4

/-- Construct the equivalence class `[f]` of an almost everywhere measurable function `f`, based
on the equivalence relation of being almost everywhere equal. -/
def mk {β : Type*} [TopologicalSpace β] (f : α → β) (hf : AEStronglyMeasurable f μ) : α →ₘ[μ] β :=
  Quotient.mk'' ⟨f, hf⟩

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