mdifferentiableWithinAt_prod_module_iff

English

In a product-module setting, differentiability within a product is equivalent to differentiability of the projections after transforming the target to the corresponding product module.

Русский

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

LaTeX

$$$\mathrm{mdifferentiableWithinAt\, prod\_module} (f)$$$

Lean4

theorem mdifferentiableWithinAt_prod_module_iff (f : M → F₁ × F₂) :
    MDifferentiableWithinAt I 𝓘(𝕜, F₁ × F₂) f s x ↔
      MDifferentiableWithinAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s x :=
  by
  rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]
  exact mdifferentiableWithinAt_prod_iff f

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