English
There is a natural embedding of the total space of the pullback bundle into B' × TotalSpace F E, given by z ↦ (z.proj, TotalSpace.mk (f z.proj) z.2).
Русский
Существует естественное вложение общего пространства вытянутого назад биндинга в B' × TotalSpace F E, заданное отображением z ↦ (proj(z), mk(f(proj(z)), snd(z))).
LaTeX
$$$$\text{pullbackTotalSpaceEmbedding}(f):\; \text{TotalSpace } F (f *^{} E) \to B' \times \text{TotalSpace } F E,\ z \mapsto (z.proj, \text{TotalSpace.mk}(f(z.proj), z.2)).$$$$
Lean4
/-- Natural embedding of the total space of `f *ᵖ E` into `B' × TotalSpace F E`. -/
@[simp]
def pullbackTotalSpaceEmbedding (f : B' → B) : TotalSpace F (f *ᵖ E) → B' × TotalSpace F E := fun z =>
(z.proj, TotalSpace.mk (f z.proj) z.2)
