comp_symm_deriv — Mathlib

English

The derivative of a differentiable OpenPartialHomeomorph e is a continuous linear equivalence between the tangent spaces: mfderiv I I' e x: TangentSpace I x ≃L[𝕜] TangentSpace I' (e x).

Русский

Производная открытого частичного гомеоморфа e задаёт непрерывное линейное эквивалентное отображение между касательными пространствами: mfderiv I I' e x.

LaTeX

$$$\mathrm{mfderiv}(I,I',e,x) : \mathrm{TangentSpace} I x \cong_L[\mathbb{K}] \mathrm{TangentSpace} I' (e x)$$$

Lean4

theorem comp_symm_deriv {x : M'} (hx : x ∈ e.target) :
    (mfderiv I I' e (e.symm x)).comp (mfderiv I' I e.symm x) = ContinuousLinearMap.id 𝕜 (TangentSpace I' x) :=
  he.symm.symm_comp_deriv hx

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