Hopf problem: elliptic · core 4

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.Elliptic.LogGauge.subtypeAction_continuousConstSMul (G : Type u_1) [Group G] {M : Type u_2} [TopologicalSpace M] [MulAction G M] (U : TopologicalSpace.Opens M) [MulAction G ↥U] (hcompat : ∀ (g : G) (x : ↥U), ↑(g • x) = g • ↑x) {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] [ChartedSpace E M] (hM : ∀ (g : G), ContMDiff (modelWithCornersSelf ℂ E) (modelWithCornersSelf ℂ E) ⊤ fun (x : M) => g • x) : ContinuousConstSMul G ↥U