Commit 2025-01-13 18:19 54f10195

View on Github →

feat(Topology/FiberBundle/Trivialization): local lifting through a Trivialization (#19056) Define versions of local lifting through a Trivialization.

Estimated changes

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

added def Trivialization.clift

added theorem Trivialization.clift_self

added def Trivialization.lift

added def Trivialization.liftCM

added theorem Trivialization.lift_self

added theorem Trivialization.proj_clift

added theorem Trivialization.proj_lift