Commit 2023-07-06 15:47 ce6df01c

View on Github →

feat: port Topology.VectorBundle.Hom (#4514)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

Created Mathlib/Topology/VectorBundle/Hom.lean

added def Bundle.ContinuousLinearMap.vectorPrebundle

added def Pretrivialization.continuousLinearMap

added def Pretrivialization.continuousLinearMapCoordChange

added theorem Pretrivialization.continuousLinearMapCoordChange_apply

added theorem Pretrivialization.continuousLinearMap_apply

added theorem Pretrivialization.continuousLinearMap_symm_apply'

added theorem Pretrivialization.continuousLinearMap_symm_apply

added theorem Pretrivialization.continuousOn_continuousLinearMapCoordChange

added theorem Trivialization.baseSet_continuousLinearMap

added def Trivialization.continuousLinearMap

added theorem Trivialization.continuousLinearMap_apply

added theorem hom_trivializationAt_apply

added theorem hom_trivializationAt_source

added theorem hom_trivializationAt_target