instCoeFun — Mathlib

English

There is a canonical CoeFun instance sending an AEEqFun to its representative function.

Русский

Существует стандартное отображение типа AEEqFun к функциям, задающее представительную функцию.

LaTeX

$$instance instCoeFun : CoeFun (α →ₘ[μ] β) (fun _ => α → β) := ⟨cast⟩$$

Lean4

/-- A measurable representative of an `AEEqFun` [f] -/
instance instCoeFun : CoeFun (α →ₘ[μ] β) fun _ => α → β :=
  ⟨cast⟩

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