Hopf problem: recognition · smale 2 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.Smale.PartialChart.bijective_mfderiv
{E : Type u_1}
{F : Type u_2}
{H : Type u_3}
{H' : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[TopologicalSpace H]
[TopologicalSpace H']
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ F H'}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace H' N]
(Φ : PartialDiffeomorph I J M N ↑⊤)
{x : M}
(hx : x ∈ Φ.source)
:
Function.Bijective ⇑(mfderiv% ↑Φ.toPartialEquiv x)