comp — Mathlib

English

If g is C^n at f(x) and f is C^n at x, then g ∘ f is C^n at x.

Русский

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

LaTeX

$$$\forall x,\; \ContDiffAt 𝕜 n g (f x) \rightarrow \ContDiffAt 𝕜 n f x \rightarrow \ContDiffAt 𝕜 n (g \circ f) x$$$

Lean4

/-- The composition of `C^n` functions at points is `C^n`. -/
nonrec theorem comp (x : E) (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (g ∘ f) x :=
  hg.comp x hf (mapsTo_univ _ _)

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