Hopf problem: foundations · local orbit quotient #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.isLocalDiffeomorphAt_congr_of_eventuallyEq
{E : Type u_1}
{F : Type u_2}
{H : Type u_3}
{K : Type u_4}
{M : Type u_5}
{N : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedAddCommGroup F]
[NormedSpace ℂ F]
[TopologicalSpace H]
[TopologicalSpace K]
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace K N]
{I : ModelWithCorners ℂ E H}
{J : ModelWithCorners ℂ F K}
{n : WithTop ℕ∞}
{f g : M → N}
{x : M}
(hf : IsLocalDiffeomorphAt I J n f x)
(hgf : g =ᶠ[nhds x] f)
:
IsLocalDiffeomorphAt I J n g x