comp_of_eq — Mathlib

English

If g is ContMDiffAt n at y and hf: f x = y with f x = y, then g ∘ f is ContMDiffAt n at x.

Русский

Если g имеет ContMDiffAt n в точке y и f x = y, тогда композиция g ∘ f имеет ContMDiffAt n в x.

LaTeX

$$$\forall {g : M' \to M''} {x : M} {y : M'}\; (hg : ContMDiffAt I' I'' n g y) (hf : ContMDiffAt I I' n f x) (hx : f x = y),\; ContMDiffAt I I'' n (g \circ f) x$$

Lean4

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

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