instInhabited

Mathlib.Geometry.Manifold.ContMDiffMap

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

English

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

Русский

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

LaTeX

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

Lean4

instance [Inhabited M'] : Inhabited C^n⟮I, M; I', M'⟯ :=
  ⟨⟨fun _ => default, contMDiff_const⟩⟩

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

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

Разделы

Аффилиация

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