comp_of_eq — Mathlib

English

If g is ContMDiffWithinAt at y and f is ContMDiffWithinAt at x with f x = y, then g∘f is ContMDiffWithinAt at x.

Русский

Если g C^n в точке y и f C^n в x и f x = y, тогда g∘f C^n в x.

LaTeX

$$$hg: ContMDiffWithinAt I' I'' n g t y, \\\\ hf: ContMDiffWithinAt I I' n f s x, \\\\ hx: f x = y \\\\Rightarrow ContMDiffWithinAt I I'' n (g \\circ f) s x$$$

Lean4

/-- See note [comp_of_eq lemmas] -/
theorem comp_of_eq {t : Set M'} {g : M' → M''} {x : M} {y : M'} (hg : ContMDiffWithinAt I' I'' n g t y)
    (hf : ContMDiffWithinAt I I' n f s x) (st : MapsTo f s t) (hx : f x = y) : ContMDiffWithinAt I I'' n (g ∘ f) s x :=
  by subst hx; exact hg.comp x hf st

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