differentiableWithinAt_pi — Mathlib

English

Differentiability of a product map is equivalent to differentiability of all coordinate maps at the point.

Русский

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

LaTeX

$$$\\text{Differentiable at } x \\iff \\forall i, \\text{Differentiable at } x \\text{ for coordinate } i.$$$

Lean4

@[simp]
theorem differentiableWithinAt_pi :
    DifferentiableWithinAt 𝕜 Φ s x ↔ ∀ i, DifferentiableWithinAt 𝕜 (fun x => Φ x i) s x :=
  ⟨fun h i => (hasFDerivWithinAt_pi'.1 h.hasFDerivWithinAt i).differentiableWithinAt, fun h =>
    (hasFDerivWithinAt_pi.2 fun i => (h i).hasFDerivWithinAt).differentiableWithinAt⟩

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