mdifferentiableWithinAt_prod_iff — Mathlib

English

If f: N → M × M′ is MF-differentiable at x, then its projections to the first and second components are MF-differentiable at x, i.e. fst and snd derivatives exist separately.

Русский

Для MF-дифференцируемости отображения f: N → M × M′ в точке x следует, что fst и snd дифференцируемы по отдельности.

LaTeX

$$$\forall\, f:\,N\to M\times M',\; \mathrm{MDifferentiableAt}(f)\Rightarrow \mathrm{MDifferentiableAt}(\mathrm{Prod.fst}\circ f) \land \mathrm{MDifferentiableAt}(\mathrm{Prod.snd}\circ f)$$$

Lean4

theorem mdifferentiableWithinAt_prod_iff (f : M → M' × N') :
    MDifferentiableWithinAt I (I'.prod J') f s x ↔
      MDifferentiableWithinAt I I' (Prod.fst ∘ f) s x ∧ MDifferentiableWithinAt I J' (Prod.snd ∘ f) s x :=
  ⟨fun h => ⟨h.fst, h.snd⟩, fun h => h.1.prodMk h.2⟩

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