Fibre-preserving maps of total spaces #
A map of total spaces Bundle.TotalSpace F₁ E₁ → Bundle.TotalSpace F₂ E₂ covering the identity of
the base is determined by its fibre maps E₁ x → E₂ x. It is bijective exactly when each of
its fibre maps is (TauCeti.bijective_totalSpace_map_iff). No topology or linear structure is
involved.
theorem
TauCeti.bijective_totalSpace_map_iff
{B : Type u_1}
{F₁ : Type u_2}
{F₂ : Type u_3}
{E₁ : B → Type u_4}
{E₂ : B → Type u_5}
{ϕ : (x : B) → E₁ x → E₂ x}
:
(Function.Bijective fun (p : Bundle.TotalSpace F₁ E₁) => Bundle.TotalSpace.mk' F₂ p.proj (ϕ p.proj p.snd)) ↔ ∀ (x : B), Function.Bijective (ϕ x)
A fibre-preserving map of total spaces is bijective exactly when each of its fibre maps is.