mdifferentiableAt_prod_module_iff

English

The differentiability of a product-valued map at a point x is equivalent to the differentiability of its coordinate projections at x.

Русский

Дифференцируемость отображения в произведении эквивалентна дифференцируемости проекций координат.

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_module_iff (f : M → F₁ × F₂) :
    MDifferentiableAt I 𝓘(𝕜, F₁ × F₂) f x ↔
      MDifferentiableAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) x ∧ MDifferentiableAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) x :=
  by
  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
  exact mdifferentiableAt_prod_iff f

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