instCoeFunForallReal — Mathlib

English

There is a canonical CoeFun instance from ContDiffBump c to real-valued functions, i.e., ContDiffBump acts as a function.

Русский

Существует каноническое соответствие ContDiffBump c с множеством вещественных функций, т. е. всплеск действует как функция.

LaTeX

$$$ \text{CoeFun}_{\mathbb{R}}(ContDiffBump(c), E \to \mathbb{R})$$$

Lean4

instance : CoeFun (ContDiffBump c) fun _ => E → ℝ :=
  ⟨toFun⟩

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