Commit 2024-11-06 07:58 c9fc36ea

View on Github →

feat: expand API of ContMDiff and MFDeriv (#18623) Sequel to #17927 and #18447.

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

added theorem contMDiffWithinAt_extChartAt_symm_range

added theorem contMDiffWithinAt_extChartAt_symm_target

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

deleted theorem ContMDiff.contMDiffOn

deleted theorem ContMDiffAt.contMDiffWithinAt

deleted theorem ContMDiffOn.contMDiffAt

added theorem ContMDiffWithinAt.congr_of_eventuallyEq_of_mem

added theorem ContMDiffWithinAt.congr_of_mem

added theorem ContMDiffWithinAt.congr_set

deleted theorem ContMDiffWithinAt.contMDiffAt

added theorem ContMDiffWithinAt.contMDiffOn'

added theorem ContMDiffWithinAt.contMDiffOn

deleted theorem ContMDiffWithinAt.insert

deleted theorem Smooth.smoothOn

deleted theorem SmoothAt.smoothWithinAt

deleted theorem SmoothOn.smoothAt

deleted theorem SmoothWithinAt.smoothAt

deleted theorem contMDiffWithinAt_congr_nhds

added theorem contMDiffWithinAt_congr_of_mem

added theorem contMDiffWithinAt_congr_set'

added theorem contMDiffWithinAt_congr_set

added theorem contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin

Modified Mathlib/Geometry/Manifold/ContMDiff/Product.lean

modified theorem contMDiffAt_prod_iff

added theorem contMDiffAt_prod_module_iff

added theorem contMDiffOn_prod_iff

added theorem contMDiffOn_prod_module_iff

modified theorem contMDiffWithinAt_prod_iff

added theorem contMDiffWithinAt_prod_module_iff

added theorem contMDiff_prod_module_iff

Modified Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_iff_of_mem

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_eventuallyEq_of_mem

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_mem

added theorem StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_set

Modified Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

added theorem ContMDiff.mdifferentiableAt

added theorem MDifferentiable.comp_mdifferentiableOn

added theorem MDifferentiable.mdifferentiableAt

added theorem MDifferentiableAt.comp_mdifferentiableWithinAt

added theorem MDifferentiableAt.comp_mdifferentiableWithinAt_of_eq

added theorem MDifferentiableAt.comp_of_eq

added theorem MDifferentiableWithinAt.comp_of_eq

added theorem MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin

added theorem MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq

added theorem MDifferentiableWithinAt.congr_nhds

added theorem MDifferentiableWithinAt.congr_of_eventuallyEq_insert

added theorem MDifferentiableWithinAt.congr_of_eventuallyEq_of_mem

added theorem MDifferentiableWithinAt.mfderivWithin_mono

added theorem MDifferentiableWithinAt.mfderivWithin_mono_of_mem_nhdsWithin

added theorem MDifferentiableWithinAt.mono_of_mem_nhdsWithin

added theorem hasMFDerivWithinAt_congr_set'

added theorem hasMFDerivWithinAt_congr_set

added theorem hasMFDerivWithinAt_diff_singleton

added theorem hasMFDerivWithinAt_insert

modified theorem mdifferentiableAt_iff_of_mem_source

added theorem mdifferentiableAt_iff_source_of_mem_source

added theorem mdifferentiableAt_iff_target

added theorem mdifferentiableAt_iff_target_of_mem_source

added theorem mdifferentiableOn_iff

added theorem mdifferentiableOn_iff_of_mem_maximalAtlas'

added theorem mdifferentiableOn_iff_of_mem_maximalAtlas

added theorem mdifferentiableOn_iff_of_subset_source'

added theorem mdifferentiableOn_iff_of_subset_source

added theorem mdifferentiableOn_iff_target

added theorem mdifferentiableWithinAt_congr_nhds

added theorem mdifferentiableWithinAt_congr_set'

added theorem mdifferentiableWithinAt_congr_set

modified theorem mdifferentiableWithinAt_iff

added theorem mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt

added theorem mdifferentiableWithinAt_iff_image

added theorem mdifferentiableWithinAt_iff_of_mem_maximalAtlas

added theorem mdifferentiableWithinAt_iff_of_mem_source'

modified theorem mdifferentiableWithinAt_iff_of_mem_source

added theorem mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas

added theorem mdifferentiableWithinAt_iff_source_of_mem_source

added theorem mdifferentiableWithinAt_iff_target

added theorem mdifferentiableWithinAt_iff_target_inter'

added theorem mdifferentiableWithinAt_iff_target_inter

added theorem mdifferentiableWithinAt_iff_target_of_mem_source

added theorem mdifferentiableWithinAt_insert

added theorem mdifferentiableWithinAt_insert_self

added theorem mdifferentiable_iff

added theorem mdifferentiable_iff_target

added theorem mfderivWithin_comp_of_eq

added theorem mfderivWithin_comp_of_preimage_mem_nhdsWithin

added theorem mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq

added theorem mfderivWithin_congr_set'

added theorem mfderivWithin_congr_set

added theorem mfderivWithin_eventually_congr_set'

added theorem mfderivWithin_eventually_congr_set

added theorem mfderiv_comp_apply

added theorem mfderiv_comp_apply_of_eq

added theorem mfderiv_comp_mfderivWithin

added theorem mfderiv_comp_mfderivWithin_of_eq

added theorem preimage_extChartAt_eventuallyEq_compl_singleton

added theorem uniqueMDiffWithinAt_iff_inter_range

Modified Mathlib/Geometry/Manifold/MFDeriv/Defs.lean

added theorem DifferentiableWithinAtProp_self

added theorem differentiableWithinAtProp_self_source

added theorem differentiableWithinAtProp_self_target