instCoeFun — Mathlib

English

There is a canonical coercion from StieltjesFunction to functions, i.e., StieltjesFunction.instCoeFun provides a function mapping to real-valued functions.

Русский

Существует каноническое отображение из StieltjesFunction в обычные функции: то есть имеется отображение-коэрционирование.

LaTeX

$$$$\\text{StieltjesFunction.instCoeFun: }\\text{StieltjesFunction} \\to (\\mathbb{R} \\to \\mathbb{R}).$$$$

Lean4

instance instCoeFun : CoeFun StieltjesFunction fun _ => ℝ → ℝ :=
  ⟨toFun⟩

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