comp_contMDiffWithinAt_of_eq — Mathlib

English

If g is ContMDiffAt 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: ContMDiffAt I' I'' n g y \\\\land hf: ContMDiffWithinAt I I' n f s x \\\\land hx: f x = y \\\\Rightarrow ContMDiffWithinAt I I'' n (g \\circ f) s x$$$

Lean4

/-- `g ∘ f` is `C^n` within `s` at `x` if `g` is `C^n` at `f x` and
`f` is `C^n` within `s` at `x`. -/
theorem comp_contMDiffWithinAt_of_eq {g : M' → M''} {x : M} {y : M'} (hg : ContMDiffAt I' I'' n g y)
    (hf : ContMDiffWithinAt I I' n f s x) (hx : f x = y) : ContMDiffWithinAt I I'' n (g ∘ f) s x := by subst hx;
  exact hg.comp_contMDiffWithinAt x hf

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