cast — Mathlib

English

Define the cast from AEEqFun to functions by selecting a representative almost everywhere equality class.

Русский

Определяем отображение cast из AEEqFun к функциям, выбирая представителя по классу почти везде равенства.

LaTeX

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

Lean4

/-- Coercion from a space of equivalence classes of almost everywhere strongly measurable
functions to functions. We ensure that if `f` has a constant representative,
then we choose that one. -/
@[coe]
def cast (f : α →ₘ[μ] β) : α → β :=
  if h : ∃ (b : β), f = mk (const α b) aestronglyMeasurable_const then const α <| Classical.choose h
  else AEStronglyMeasurable.mk _ (Quotient.out f : { f : α → β // AEStronglyMeasurable f μ }).2

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