uniqueMDiffOn — Mathlib

English

If g is differentiable at f(x) and f is MDifferentiableAt at x, then g ∘ f is MDifferentiableAt at x.

Русский

Если g дифференцируемо в точке f(x) и f дифференцируема в точке x, то композиция g∘f дифференцируема в x.

LaTeX

$$$\text{DifferentiableAt}(g, f(x)) \land \text{MDifferentiableAt}(f,x) \rightarrow \text{MDifferentiableAt}(g\circ f, x).$$$

Lean4

theorem uniqueMDiffOn {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) :
    UniqueMDiffOn 𝓘(𝕜, E) (Set.range I) :=
  I.uniqueDiffOn.uniqueMDiffOn

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