toFun — Mathlib

English

There is a canonical ContMDiffMul instance, ensuring smooth multiplication on R from a ContMDiffRing.

Русский

Существует канонический инстанс ContMDiffMul, обеспечивающий гладкость умножения на R.

LaTeX

$$$\\text{ContMDiffMul } I\\; n\\; R$$$

Lean4

/-- The function defined by `f : SmoothBumpFunction c`. Use automatic coercion to function
instead. -/
@[coe]
def toFun : M → ℝ :=
  indicator (chartAt H c).source (f.toContDiffBump ∘ extChartAt I c)

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