Commit 2023-05-18 07:49 c01ffda0

View on Github →

feat: port Topology.FiberBundle.Constructions (#3145)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/FiberBundle/Constructions.lean

added theorem Bundle.Trivial.eq_trivialization

added def Bundle.Trivial.trivialization

added theorem Bundle.Trivial.trivialization_source

added theorem Bundle.Trivial.trivialization_target

added theorem FiberBundle.Prod.inducing_diag

added theorem Pullback.continuous_lift

added theorem Pullback.continuous_proj

added theorem Pullback.continuous_totalSpaceMk

added theorem Trivialization.Prod.continuous_inv_fun

added theorem Trivialization.Prod.continuous_to_fun

added theorem Trivialization.Prod.left_inv

added theorem Trivialization.Prod.right_inv

added def Trivialization.Prod.toFun'

added theorem Trivialization.baseSet_prod

added theorem Trivialization.prod_symm_apply

added theorem inducing_pullbackTotalSpaceEmbedding