toContDiffMapSupportedInClass — Mathlib

English

The coe projection coincides with the underlying function of a ContDiffMapSupportedIn object.

Русский

Проекция коэрции совпадает с базовой функцией объекта ContDiffMapSupportedIn.

LaTeX

$$$$f.toFun = (f : E \\to F).$$$$

Lean4

instance toContDiffMapSupportedInClass : ContDiffMapSupportedInClass 𝓓^{n}_{K}(E, F) E F n K
    where
  coe f := f.toFun
  coe_injective' f g h := by cases f; cases g; congr
  map_contDiff f := f.contDiff'
  map_zero_on_compl f := f.zero_on_compl'

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