Hopf problem: foundations · fibre topology

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

theorem Mathoverflow1973.FibreTopology.fibre_isConnected_comp_homeomorph {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Y) (e : Y ≃ₜ Z) (b : Z) (h : IsConnected (f ⁻¹' {e.symm b})) : IsConnected (⇑e ∘ f ⁻¹' {b})