comp_of_preimage_mem_nhdsWithin_of_eq

English

If the hypotheses hold with equality f(x) = y, then the composition g ∘ f is ContDiffWithinAt.

Русский

Если выполняются условия с равенством f(x) = y, то композиция g ∘ f имеет ContDiffWithinAt.

LaTeX

$$$\forall x\in E,\; \ContDiffWithinAt 𝕜 n\; g\; t\; y\; \rightarrow\; \ContDiffWithinAt 𝕜 n\; f\; s\; x\; \rightarrow\; f x = y \rightarrow\ ContDiffWithinAt 𝕜 n\; (g \circ f)\; s\; x$$$

Lean4

/-- The composition of `C^n` functions at points in domains is `C^n`,
  with a weaker condition on `s` and `t`. -/
theorem comp_of_preimage_mem_nhdsWithin_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) (hs : f ⁻¹' t ∈ 𝓝[s] x) (hy : f x = y) :
    ContDiffWithinAt 𝕜 n (g ∘ f) s x := by subst hy; exact hg.comp_of_preimage_mem_nhdsWithin x hf hs

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