prodMap — Mathlib

English

For f: M → M' × N' the differentiability (MDifferentiable) is equivalent to differentiability of the two coordinate maps.

Русский

Для отображения f: M → M' × N' дифференцируемость эквивалентна дифференцируемости двух координатных отображений.

LaTeX

$$$\text{MDifferentiable } I (I'.prod J') f \iff (\text{MDifferentiable } I I' (\mathrm{Prod.fst} \circ f) \land \text{MDifferentiable } I J' (\mathrm{Prod.snd} \circ f))$$$

Lean4

theorem prodMap (hf : MDifferentiable I I' f) (hg : MDifferentiable J J' g) :
    MDifferentiable (I.prod J) (I'.prod J') (Prod.map f g) := fun p ↦ (hf p.1).prodMap' (hg p.2)

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