instContinuousMapClass

Mathlib.Geometry.Manifold.ContMDiffMap

URI: https://scilib.ai/kg/mathlib#ContMDiffMap.instContinuousMapClass

English

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

Русский

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

LaTeX

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

Lean4

instance : ContinuousMapClass C^n⟮I, M; I', M'⟯ M M' where map_continuous f := f.contMDiff.continuous

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

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

Разделы

Аффилиация

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