Hopf problem: foundations · two open transition

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

theorem Mathoverflow1973.CoveringComposition.covering_comp_of_finite_fibres {E : Type u_1} {B : Type u_2} {X : Type u_3} [TopologicalSpace E] [TopologicalSpace B] [TopologicalSpace X] {f : E → B} {g : B → X} (hf : IsCoveringMap f) (hg : IsCoveringMap g) (hfin : ∀ (x : X), Finite ↑(g ⁻¹' {x})) : IsCoveringMap (g ∘ f)