contMDiffWithinAt_univ — Mathlib

English

Equivalently, ContMDiffAt I I' n f x holds exactly when f is continuous at x and its coordinate expression is C^n inside charts.

Русский

Эквивалентно: ContMDiffAt эквивалентно непрерывности в x и координатному выражению, являющемуся C^n в графах.

LaTeX

$$$ContMDiffAt\, I\, I'\, n\, f\, x \;\iff\; (ContinuousAt\, f\, x) \wedge (ContDiffWithinAt\, 𝕜\, n\, (extChartAt I' (f x) \circ f) \; \text{на} \, (range I) \; (extChartAt I x x))$$$

Lean4

theorem contMDiffWithinAt_univ : ContMDiffWithinAt I I' n f univ x ↔ ContMDiffAt I I' n f x :=
  Iff.rfl

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