mdifferentiable_fst — Mathlib

English

Let I, I′ be charts on M and M′, respectively. The first projection Prod.fst: M × M′ → M is MF-differentiable globally, i.e. MDifferentiable (I.prod I′) I Prod.fst.

Русский

Пусть I и I′ — карты на M и M′. Первая проекция Prod.fst: M × M′ → M дифференцируема в MF-слове глобально.

LaTeX

$$$\mathrm{MDifferentiable}(I\prod I',\,I,\,\mathrm{Prod.fst})$$$

Lean4

theorem mdifferentiable_fst : MDifferentiable (I.prod I') I (Prod.fst : M × M' → M) := fun _ => mdifferentiableAt_fst

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