Commit 2023-01-04 18:33 047e52ab

View on Github →

feat: port Data.Bundle (#1288) Not sure what to do with:

set_option quotPrecheck false in
/-- The canonical projection defining a bundle. -/
scoped notation "π" => @Bundle.TotalSpace.proj _

But otherwise what seems like a fairly straightforward port.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Bundle.lean

added def Bundle.Pullback.lift

added theorem Bundle.Pullback.lift_mk

added theorem Bundle.Pullback.proj_lift

added def Bundle.Pullback

added theorem Bundle.TotalSpace.eta

added theorem Bundle.TotalSpace.mk_cast

added def Bundle.TotalSpace.proj

added theorem Bundle.TotalSpace.proj_mk

added def Bundle.TotalSpace

added def Bundle.Trivial.projSnd

added def Bundle.Trivial

added theorem Bundle.coe_fst

added theorem Bundle.coe_snd

added theorem Bundle.coe_snd_map_apply

added theorem Bundle.coe_snd_map_smul

added def Bundle.pullbackTotalSpaceEmbedding

added theorem Bundle.pullbackTotalSpaceEmbedding_snd

added theorem Bundle.sigma_mk_eq_totalSpaceMk

added def Bundle.totalSpaceMk