Theorem Trivialization.mdifferentiableWithinAt_snd_comp_iff₂

Modification history

2025-09-15 19:33
Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
feat: mdifferentiableOn_section_of_mem_baseSet₀ (#26870) …
Added Trivialization.mdifferentiableWithinAt_snd_comp_iff₂View on Github →