comp_of_eq — Mathlib

English

If hg : ContDiffWithinAt 𝕜 n g t and hf : ContDiffWithinAt 𝕜 n f s x, and s ∩ f^{-1}(t) is considered, then g ∘ f is ContDiffWithinAt 𝕜 n on s ∩ f^{-1}(t).

Русский

Если g и f гладкие внутри соответствующих множеств и рассматривается пересечение, то композиция гладкая внутри пересечения.

LaTeX

$$$ \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} (g \circ f)\ (s \cap f^{-1}(t))$$$

Lean4

/-- The composition of `C^n` functions at points in domains is `C^n`. -/
theorem comp_of_eq {s : Set E} {t : Set F} {g : F → G} {f : E → F} {y : F} (x : E) (hg : ContDiffWithinAt 𝕜 n g t y)
    (hf : ContDiffWithinAt 𝕜 n f s x) (st : MapsTo f s t) (hy : f x = y) : ContDiffWithinAt 𝕜 n (g ∘ f) s x := by
  subst hy; exact hg.comp x hf st

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