Commit 2023-06-26 19:57 401515fc

View on Github →

feat: port Geometry.Manifold.Mfderiv (#5454)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/MFDeriv.lean

added theorem ContMDiff.mdifferentiable

added theorem ContMDiffAt.mdifferentiableAt

added theorem ContMDiffOn.mdifferentiableOn

added theorem ContMDiffWithinAt.mdifferentiableWithinAt

added theorem ContinuousLinearEquiv.mfderivWithin_eq

added theorem ContinuousLinearEquiv.mfderiv_eq

added theorem ContinuousLinearMap.mfderivWithin_eq

added theorem ContinuousLinearMap.mfderiv_eq

added def DifferentiableWithinAtProp

added theorem Filter.EventuallyEq.mdifferentiableWithinAt_iff

added theorem Filter.EventuallyEq.mfderivWithin_eq

added theorem Filter.EventuallyEq.mfderiv_eq

added theorem HasMFDerivAt.add

added theorem HasMFDerivAt.comp

added theorem HasMFDerivAt.comp_hasMFDerivWithinAt

added theorem HasMFDerivAt.congr_of_eventuallyEq

added theorem HasMFDerivAt.const_smul

added theorem HasMFDerivAt.continuousAt

added theorem HasMFDerivAt.hasMFDerivWithinAt

added theorem HasMFDerivAt.mdifferentiableAt

added theorem HasMFDerivAt.mul'

added theorem HasMFDerivAt.mul

added theorem HasMFDerivAt.neg

added theorem HasMFDerivAt.sub

added def HasMFDerivAt

added theorem HasMFDerivWithinAt.comp

added theorem HasMFDerivWithinAt.congr_mono

added theorem HasMFDerivWithinAt.congr_of_eventuallyEq

added theorem HasMFDerivWithinAt.continuousWithinAt

added theorem HasMFDerivWithinAt.hasMFDerivAt

added theorem HasMFDerivWithinAt.mdifferentiableWithinAt

added theorem HasMFDerivWithinAt.mfderivWithin

added theorem HasMFDerivWithinAt.mono

added theorem HasMFDerivWithinAt.mul'

added theorem HasMFDerivWithinAt.mul

added theorem HasMFDerivWithinAt.nhdsWithin

added theorem HasMFDerivWithinAt.union

added def HasMFDerivWithinAt

added theorem IsOpen.uniqueMDiffOn

added theorem IsOpen.uniqueMDiffWithinAt

added theorem LocalHomeomorph.MDifferentiable.comp_symm_deriv

added theorem LocalHomeomorph.MDifferentiable.ker_mfderiv_eq_bot

added theorem LocalHomeomorph.MDifferentiable.mdifferentiableAt_symm

added theorem LocalHomeomorph.MDifferentiable.mfderiv_bijective

added theorem LocalHomeomorph.MDifferentiable.mfderiv_injective

added theorem LocalHomeomorph.MDifferentiable.mfderiv_surjective

added theorem LocalHomeomorph.MDifferentiable.range_mfderiv_eq_top

added theorem LocalHomeomorph.MDifferentiable.range_mfderiv_eq_univ

added theorem LocalHomeomorph.MDifferentiable.symm_comp_deriv

added theorem LocalHomeomorph.MDifferentiable.trans

added def LocalHomeomorph.MDifferentiable

added theorem MDifferentiable.add

added theorem MDifferentiable.comp

added theorem MDifferentiable.const_smul

added theorem MDifferentiable.continuous

added theorem MDifferentiable.mdifferentiableOn

added theorem MDifferentiable.mfderivWithin

added theorem MDifferentiable.mul

added theorem MDifferentiable.neg

added theorem MDifferentiable.prod_mk

added theorem MDifferentiable.prod_mk_space

added theorem MDifferentiable.sub

added def MDifferentiable

added theorem MDifferentiableAt.add

added theorem MDifferentiableAt.comp

added theorem MDifferentiableAt.congr_of_eventuallyEq

added theorem MDifferentiableAt.const_smul

added theorem MDifferentiableAt.continuousAt

added theorem MDifferentiableAt.hasMFDerivAt

added theorem MDifferentiableAt.mdifferentiableWithinAt

added theorem MDifferentiableAt.mfderiv_prod

added theorem MDifferentiableAt.mul

added theorem MDifferentiableAt.neg

added theorem MDifferentiableAt.prod_mk

added theorem MDifferentiableAt.prod_mk_space

added theorem MDifferentiableAt.sub

added def MDifferentiableAt

added theorem MDifferentiableOn.comp

added theorem MDifferentiableOn.congr_mono

added theorem MDifferentiableOn.continuousOn

added theorem MDifferentiableOn.mono

added theorem MDifferentiableOn.mul

added theorem MDifferentiableOn.prod_mk

added theorem MDifferentiableOn.prod_mk_space

added def MDifferentiableOn

added theorem MDifferentiableWithinAt.comp

added theorem MDifferentiableWithinAt.congr

added theorem MDifferentiableWithinAt.congr_mono

added theorem MDifferentiableWithinAt.congr_of_eventuallyEq

added theorem MDifferentiableWithinAt.continuousWithinAt

added theorem MDifferentiableWithinAt.hasMFDerivWithinAt

added theorem MDifferentiableWithinAt.mdifferentiableAt

added theorem MDifferentiableWithinAt.mfderivWithin_congr_mono

added theorem MDifferentiableWithinAt.mono

added theorem MDifferentiableWithinAt.mul

added theorem MDifferentiableWithinAt.prod_mk

added theorem MDifferentiableWithinAt.prod_mk_space

added def MDifferentiableWithinAt

added theorem ModelWithCorners.hasMFDerivWithinAt_symm

added theorem ModelWithCorners.mdifferentiableOn_symm

added theorem Smooth.mdifferentiable

added theorem Smooth.mdifferentiableAt

added theorem Smooth.mdifferentiableWithinAt

added theorem Trivialization.mdifferentiable

added theorem UniqueMDiffOn.eq

added theorem UniqueMDiffOn.image_denseRange'

added theorem UniqueMDiffOn.image_denseRange

added theorem UniqueMDiffOn.inter

added theorem UniqueMDiffOn.prod

added theorem UniqueMDiffOn.smooth_bundle_preimage

added theorem UniqueMDiffOn.tangentBundle_proj_preimage

added theorem UniqueMDiffOn.uniqueDiffOn_inter_preimage

added theorem UniqueMDiffOn.uniqueDiffOn_target_inter

added theorem UniqueMDiffOn.uniqueMDiffOn_preimage

added def UniqueMDiffOn

added theorem UniqueMDiffWithinAt.image_denseRange

added theorem UniqueMDiffWithinAt.inter'

added theorem UniqueMDiffWithinAt.inter

added theorem UniqueMDiffWithinAt.mono

added theorem UniqueMDiffWithinAt.mono_of_mem

added theorem UniqueMDiffWithinAt.smooth_bundle_preimage'

added theorem UniqueMDiffWithinAt.smooth_bundle_preimage

added def UniqueMDiffWithinAt

added theorem const_smul_mfderiv

added theorem differentiable_within_at_localInvariantProp

added theorem hasMFDerivAt_const

added theorem hasMFDerivAt_extChartAt

added theorem hasMFDerivAt_fst

added theorem hasMFDerivAt_id

added theorem hasMFDerivAt_iff_hasFDerivAt

added theorem hasMFDerivAt_neg

added theorem hasMFDerivAt_snd

added theorem hasMFDerivAt_unique

added theorem hasMFDerivWithinAt_const

added theorem hasMFDerivWithinAt_extChartAt

added theorem hasMFDerivWithinAt_fst

added theorem hasMFDerivWithinAt_id

added theorem hasMFDerivWithinAt_iff_hasFDerivWithinAt

added theorem hasMFDerivWithinAt_inter'

added theorem hasMFDerivWithinAt_inter

added theorem hasMFDerivWithinAt_snd

added theorem hasMFDerivWithinAt_univ

added theorem mdifferentiableAt_atlas

added theorem mdifferentiableAt_atlas_symm

added theorem mdifferentiableAt_const

added theorem mdifferentiableAt_extChartAt

added theorem mdifferentiableAt_fst

added theorem mdifferentiableAt_id

added theorem mdifferentiableAt_iff_differentiableAt

added theorem mdifferentiableAt_iff_liftPropAt

added theorem mdifferentiableAt_iff_of_mem_source

added theorem mdifferentiableAt_neg

added theorem mdifferentiableAt_snd

added theorem mdifferentiableOn_atlas

added theorem mdifferentiableOn_atlas_symm

added theorem mdifferentiableOn_const

added theorem mdifferentiableOn_extChartAt

added theorem mdifferentiableOn_fst

added theorem mdifferentiableOn_id

added theorem mdifferentiableOn_iff_differentiableOn

added theorem mdifferentiableOn_of_locally_mdifferentiableOn

added theorem mdifferentiableOn_snd

added theorem mdifferentiableOn_univ

added theorem mdifferentiableWithinAt_const

added theorem mdifferentiableWithinAt_fst

added theorem mdifferentiableWithinAt_id

added theorem mdifferentiableWithinAt_iff

added theorem mdifferentiableWithinAt_iff_differentiableWithinAt

added theorem mdifferentiableWithinAt_iff_liftPropWithinAt

added theorem mdifferentiableWithinAt_iff_of_mem_source

added theorem mdifferentiableWithinAt_inter'

added theorem mdifferentiableWithinAt_inter

added theorem mdifferentiableWithinAt_snd

added theorem mdifferentiableWithinAt_univ

added theorem mdifferentiable_chart

added theorem mdifferentiable_const

added theorem mdifferentiable_fst

added theorem mdifferentiable_id

added theorem mdifferentiable_iff_differentiable

added theorem mdifferentiable_of_mem_atlas

added theorem mdifferentiable_snd

added def mfderiv

added def mfderivWithin

added theorem mfderivWithin_comp

added theorem mfderivWithin_congr

added theorem mfderivWithin_const

added theorem mfderivWithin_eq_fderivWithin

added theorem mfderivWithin_fst

added theorem mfderivWithin_id

added theorem mfderivWithin_inter

added theorem mfderivWithin_snd

added theorem mfderivWithin_subset

added theorem mfderivWithin_univ

added theorem mfderivWithin_zero_of_not_mdifferentiableWithinAt

added theorem mfderiv_add

added theorem mfderiv_comp

added theorem mfderiv_comp_of_eq

added theorem mfderiv_congr

added theorem mfderiv_congr_point

added theorem mfderiv_const

added theorem mfderiv_eq_fderiv

added theorem mfderiv_fst

added theorem mfderiv_id

added theorem mfderiv_neg

added theorem mfderiv_prod_eq_add

added theorem mfderiv_prod_left

added theorem mfderiv_prod_right

added theorem mfderiv_snd

added theorem mfderiv_sub

added theorem mfderiv_zero_of_not_mdifferentiableAt

added def tangentMap

added def tangentMapWithin

added theorem tangentMapWithin_comp_at

added theorem tangentMapWithin_congr

added theorem tangentMapWithin_eq_tangentMap

added theorem tangentMapWithin_fst

added theorem tangentMapWithin_id

added theorem tangentMapWithin_prod_fst

added theorem tangentMapWithin_prod_snd

added theorem tangentMapWithin_proj

added theorem tangentMapWithin_subset

added theorem tangentMapWithin_univ

added theorem tangentMap_chart

added theorem tangentMap_chart_symm

added theorem tangentMap_comp

added theorem tangentMap_comp_at

added theorem tangentMap_fst

added theorem tangentMap_id

added theorem tangentMap_prod_fst

added theorem tangentMap_prod_snd

added theorem tangentMap_proj

added theorem uniqueMDiffOn_iff_uniqueDiffOn

added theorem uniqueMDiffOn_univ

added theorem uniqueMDiffWithinAt_iff

added theorem uniqueMDiffWithinAt_iff_uniqueDiffWithinAt

added theorem uniqueMDiffWithinAt_univ

added theorem writtenInExtChartAt_comp

added theorem writtenInExtChartAt_model_space