fst

Mathlib.Geometry.Manifold.ContMDiffMap

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

English

Two ContMDiffMaps are equal if they are equal pointwise.

Русский

Два отображения ContMDiffMap равны, если они равны на каждой точке.

LaTeX

$$$\forall x, f x = g x \Rightarrow f = g$$$

Lean4

/-- The first projection of a product, as a `C^n` map. -/
def fst : C^n⟮I.prod I', M × M'; I, M⟯ :=
  ⟨Prod.fst, contMDiff_fst⟩

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

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

Разделы

Аффилиация

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