continuous_tangentMap — Mathlib

English

If f is C^n, then its tangent map is C^m: the smoothness lifts to tangent level.

Русский

Если f гладкое, то tangentMap гладко в касательном уровне.

LaTeX

$$$\forall hf : ContMDiff I I' n f,\ hmn : m + 1 ≤ n \Rightarrow ContMDiff I.tangent I'.tangent m (tangentMap I I' f)$$$

Lean4

/-- If a function is `C^n`, with `1 ≤ n`, then its bundled derivative is continuous. -/
theorem continuous_tangentMap (hf : ContMDiff I I' n f) (hmn : 1 ≤ n) : Continuous (tangentMap I I' f) :=
  by
  rw [← contMDiffOn_univ] at hf
  rw [← continuousOn_univ]
  convert hf.continuousOn_tangentMapWithin hmn uniqueMDiffOn_univ
  rw [tangentMapWithin_univ]

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