Commit 2023-06-24 05:35 50336a5b

View on Github →

feat: port Geometry.Manifold.VectorBundle.FiberwiseLinear (#5440)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean

added def FiberwiseLinear.localHomeomorph

added theorem FiberwiseLinear.source_trans_localHomeomorph

added theorem FiberwiseLinear.target_trans_localHomeomorph

added theorem FiberwiseLinear.trans_localHomeomorph_apply

added theorem SmoothFiberwiseLinear.locality_aux₁

added theorem SmoothFiberwiseLinear.locality_aux₂

added theorem mem_smoothFiberwiseLinear_iff

added def smoothFiberwiseLinear