contDiffAt_inner — Mathlib

English

For any p = (f,g) in E×E, ContDiffAt Real n (p ↦ ⟪f,g⟫) at p holds if f and g are ContDiffAt Real n at the corresponding entries.

Русский

Для любого p = (f,g) в E×E верно ContDiffAt Real n для отображения p ↦ ⟪f,g⟫, если f и g имеют ContDiffAt Real n на точке p.

LaTeX

$$$\\operatorname{ContDiffAt}_{\\mathbb{R}} n\\bigl(p \\mapsto \\langle p_1, p_2\\rangle\\bigr)(p).$$$

Lean4

theorem contDiffAt_inner {p : E × E} {n} : ContDiffAt ℝ n (fun p : E × E => ⟪p.1, p.2⟫) p :=
  ContDiff.contDiffAt contDiff_inner

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