English
If f is C^n on a set s, then the tangent map within of f is C^m on the preimage of s under the tangent projection.
Русский
Если f гладкое на s, то tangentMapWithin(f) гладко на прообразе s через проекцию касательного пространства.
LaTeX
$$$\forall hf : ContMDiffOn I I' n f s,\ hmn : 1 ≤ n,\ hs : UniqueMDiffOn I s \Rightarrow ContinuousOn (tangentMapWithin I I' f s) (π E(TangentSpace I)^{-1}' s)$$$
Lean4
/-- If a function is `C^n` on a domain with unique derivatives, with `1 ≤ n`, then its bundled
derivative is continuous there. -/
theorem continuousOn_tangentMapWithin (hf : ContMDiffOn I I' n f s) (hmn : 1 ≤ n) (hs : UniqueMDiffOn I s) :
ContinuousOn (tangentMapWithin I I' f s) (π E(TangentSpace I) ⁻¹' s) :=
by
have : ContMDiffOn I.tangent I'.tangent 0 (tangentMapWithin I I' f s) (π E(TangentSpace I) ⁻¹' s) :=
hf.contMDiffOn_tangentMapWithin hmn hs
exact this.continuousOn
