Theorem contMDiffOn_section_of_mem_baseSet₀

Modification history

2025-09-15 19:33
Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
feat: mdifferentiableOn_section_of_mem_baseSet₀ (#26870) …
Deleted contMDiffOn_section_of_mem_baseSet₀View on Github →
2025-07-05 17:25
Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
feat: contMDiffOn_section_of_mem_baseSet (#26678) …
Added contMDiffOn_section_of_mem_baseSet₀View on Github →