Hopf problem: foundations · triangle regular base fundamental group #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.SimplyConnectedCover.trans_mem
{X : Type u_1}
[TopologicalSpace X]
{s : Set X}
{x y z : X}
(p : Path x y)
(q : Path y z)
(hp : ∀ (t : ↑unitInterval), p t ∈ s)
(hq : ∀ (t : ↑unitInterval), q t ∈ s)
(t : ↑unitInterval)
: