const

Mathlib.Geometry.Manifold.ContMDiffMap

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

English

The second projection of a product is a C^n map.

Русский

Вторая проекция произведения является C^n отображением.

LaTeX

$$$\text{snd} : C^n⟮I.prod I', M × M'; I', M'⟯ := ⟨Prod.snd, contMDiff_snd⟩$$$

Lean4

/-- Constant map as a `C^n` map -/
def const (y : M') : C^n⟮I, M; I', M'⟯ :=
  ⟨fun _ => y, contMDiff_const⟩

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

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

Разделы

Аффилиация

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