comp_contDiffWithinAt — Mathlib

English

If g is C^n (even just ContDiff) and f is C^n within s at x, then g ∘ f is C^n within s at x.

Русский

Если g имеет класс C^n (ContDiff) и f имеет класс C^n внутри s в точке x, то g ∘ f имеет класс C^n внутри s в x.

LaTeX

$$$\forall x\in E,\; \ContDiff 𝕜 n g \rightarrow \ContDiffWithinAt 𝕜 n f s x \rightarrow \ContDiffWithinAt 𝕜 n (g \circ f) s x$$$

Lean4

theorem comp_contDiffWithinAt (x : E) (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffWithinAt 𝕜 n f s x) :
    ContDiffWithinAt 𝕜 n (g ∘ f) s x :=
  hg.comp x hf (mapsTo_univ _ _)

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