English
The total space of the fiberwise product of two bundles E1 and E2 is equipped with the topology induced from the diagonal embedding into TotalSpace F1 E1 × TotalSpace F2 E2.
Русский
Общее пространство фибрового произведения E1 ×ᵇ E2 снабжено топологией, полученной порожденной диагональным вложением в TotalSpace F1 E1 × TotalSpace F2 E2.
LaTeX
$$$\mathrm{TopologicalSpace}\big(\mathrm{TotalSpace}(F_1 \times F_2)(E_1 \times^{\mathrm{b}} E_2)\big) = \mathrm{TopologicalSpace.induced}\left(\lambda p, (\langle p.1, p.2.1\rangle, \langle p.1, p.2.2\rangle)\right)$$$
Lean4
/-- Equip the total space of the fiberwise product of two fiber bundles `E₁`, `E₂` with
the induced topology from the diagonal embedding into `TotalSpace F₁ E₁ × TotalSpace F₂ E₂`. -/
instance topologicalSpace : TopologicalSpace (TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂)) :=
TopologicalSpace.induced (fun p ↦ ((⟨p.1, p.2.1⟩ : TotalSpace F₁ E₁), (⟨p.1, p.2.2⟩ : TotalSpace F₂ E₂)))
inferInstance
