mdifferentiableAt_prod_iff — Mathlib

English

For f: M → M′ × N′, differentiability at x is equivalent to differentiability of Prod.fst ∘ f at x and Prod.snd ∘ f at x.

Русский

Для f: M → M′ × N′, дифференцируемость в точке эквивалентна дифференцируемости по координатам.

LaTeX

$$$\mathrm{MDifferentiableAt}\, I\, (I'.prod J')\, f\, x \iff \mathrm{MDifferentiableAt}\, I I' (\mathrm{Prod.fst} \circ f)\, x \land \mathrm{MDifferentiableAt}\, I J' (\mathrm{Prod.snd} \circ f)\, x$$$

Lean4

theorem mdifferentiableAt_prod_iff (f : M → M' × N') :
    MDifferentiableAt I (I'.prod J') f x ↔
      MDifferentiableAt I I' (Prod.fst ∘ f) x ∧ MDifferentiableAt I J' (Prod.snd ∘ f) x :=
  by simp_rw [← mdifferentiableWithinAt_univ]; exact mdifferentiableWithinAt_prod_iff f

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