Hopf problem: toric · diagonal quotient 3 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.DiagonalQuotient.baseSection_openEmbedding
{G : Type u_1}
{B : Type u_2}
[Group G]
[MulAction G B]
[TopologicalSpace B]
(hq : IsQuotientCoveringMap (baseQuotient G B) G)
(U : TopologicalSpace.Opens (BaseSpace G B))
(s : C(↥U, B))
(hs : ∀ (x : ↥U), baseQuotient G B (s x) = ↑x)
: