Commit 2025-06-19 19:33 8ec0f931

View on Github →

feat: applying a smooth hom bundle section to a smooth section gives a smooth section (#26112)

Estimated changes

Modified Mathlib/Geometry/Manifold/VectorBundle/Hom.lean

added theorem ContMDiff.clm_bundle_apply

added theorem ContMDiff.clm_bundle_apply₂

added theorem ContMDiffAt.clm_bundle_apply

added theorem ContMDiffAt.clm_bundle_apply₂

added theorem ContMDiffOn.clm_bundle_apply

added theorem ContMDiffOn.clm_bundle_apply₂

added theorem ContMDiffWithinAt.clm_bundle_apply

added theorem ContMDiffWithinAt.clm_bundle_apply₂

modified theorem contMDiffAt_hom_bundle

added theorem contMDiffWithinAt_hom_bundle

Modified Mathlib/Topology/VectorBundle/Hom.lean