contDiffAt_pi — Mathlib

English

A Pi-structured function Φ: E → ∀ i, F'_i is ContDiffAt n at x iff each coordinate Φ x i is ContDiffAt n at x.

Русский

Функция Φ: E → ∀ i, F'_i имеет ContDiffAt n в точке x тогда и только тогда каждая координата Φ x i имеет ContDiffAt n в x.

LaTeX

$$$ ContDiffAt 𝕜 n Φ x \iff \forall i, ContDiffAt 𝕜 n (\\lambda x. Φ x i) x $$$

Lean4

theorem contDiffAt_pi : ContDiffAt 𝕜 n Φ x ↔ ∀ i, ContDiffAt 𝕜 n (fun x => Φ x i) x :=
  contDiffWithinAt_pi

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