Hopf problem: recognition · smale 8 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.Smale.ManifoldImmersion.exists_compact_boundary_derivative_repair
{B : Type u_1}
{E : Type u_2}
{G : Type u_3}
{H : Type u_4}
{H' : Type u_5}
{X : Type u_6}
{N : Type u_7}
[NormedAddCommGroup B]
[NormedSpace ℝ B]
[FiniteDimensional ℝ B]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[TopologicalSpace H]
[TopologicalSpace H']
{I : ModelWithCorners ℝ B H}
{J : ModelWithCorners ℝ G H'}
[J.Boundaryless]
[TopologicalSpace X]
[ChartedSpace H X]
[IsManifold I (↑⊤) X]
[CompactSpace X]
[LindelofSpace (X × E)]
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J (↑⊤) N]
(f : C(E, N))
(hf : ContMDiff (modelWithCornersSelf ℝ E) J ↑⊤ ⇑f)
{b : X → E}
(hb : ContMDiff I (modelWithCornersSelf ℝ E) (↑⊤) b)
{ρ : E → ℝ}
(hρ : ContDiff ℝ (↑⊤) ρ)
(hzero : ∀ (x : X), ρ (b x) = 0)
(hdim : Module.finrank ℝ B + Module.finrank ℝ E < Module.finrank ℝ G)
(hcommon :
∀ (y : E),
ρ y = 0 → ∀ (v : TangentSpace (modelWithCornersSelf ℝ E) y), (mfderiv% ⇑f y) v = 0 → (fderiv ℝ ρ y) v = 0 → v = 0)
: