English
For x ∈ e.source, the derivative mfderiv I I' e x is bijective.
Русский
Для x ∈ области определения отображение mfderiv I I' e x биективно.
LaTeX
$$$\text{Function.Bijective}(mfderiv\,I\,I'\,e\,x)$$$
Lean4
/-- The derivative of a differentiable open partial homeomorphism, as a continuous linear
equivalence between the tangent spaces at `x` and `e x`. -/
protected def mfderiv (he : e.MDifferentiable I I') {x : M} (hx : x ∈ e.source) :
TangentSpace I x ≃L[𝕜] TangentSpace I' (e x) :=
{ mfderiv I I' e x with
invFun := mfderiv I' I e.symm (e x)
continuous_toFun := (mfderiv I I' e x).cont
continuous_invFun := (mfderiv I' I e.symm (e x)).cont
left_inv := fun y =>
by
have : (ContinuousLinearMap.id _ _ : TangentSpace I x →L[𝕜] TangentSpace I x) y = y := rfl
conv_rhs => rw [← this, ← he.symm_comp_deriv hx]
rfl
right_inv := fun y =>
by
have : (ContinuousLinearMap.id 𝕜 _ : TangentSpace I' (e x) →L[𝕜] TangentSpace I' (e x)) y = y := rfl
conv_rhs => rw [← this, ← he.comp_symm_deriv (e.map_source hx)]
rw [e.left_inv hx]
rfl }
