Theorem ContMDiffWithinAt.clm_bundle_apply₂

Modification history

2025-06-19 19:33

Mathlib/Geometry/Manifold/VectorBundle/Hom.lean

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

Added ContMDiffWithinAt.clm_bundle_apply₂ View on Github →