hasCoeToContMDiffMap

Mathlib.Geometry.Manifold.ContMDiffMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.hasCoeToContMDiffMap

English

C^n-maps form a ContinuousMapClass of maps M → M'.

Русский

Класс отображений C^n образует класс непрерывных отображений M → M'.

LaTeX

$$$\text{instance } \text{ContinuousMapClass } (C^n⟮I, M; I', M'⟯) M M'$$$

Lean4

instance hasCoeToContMDiffMap : Coe (E →L[𝕜] E') C^n⟮𝓘(𝕜, E), E; 𝓘(𝕜, E'), E'⟯ :=
  ⟨fun f => ⟨f, f.contMDiff⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru