Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-17 03:02 9ac26cb6

View on Github →

feat(geometry/manifold/mfderiv): derivative of functions between smooth manifolds (#1872)

  • feat(geometry/manifold/mfderiv): derivative of functions between smooth manifolds
  • Update src/geometry/manifold/mfderiv.lean Co-Authored-By: Yury G. Kudryashov [email protected]
  • more details in docstrings [ci skip]
  • fix docstrings [ci skip]
  • reviewer's comments

Estimated changes

added def bundle_mfderiv
added theorem bundle_mfderiv_comp
added theorem bundle_mfderiv_comp_at
added theorem bundle_mfderiv_proj
added theorem has_mfderiv_at.comp
added theorem has_mfderiv_at.mfderiv
added def has_mfderiv_at
added theorem has_mfderiv_at_const
added theorem has_mfderiv_at_id
added theorem has_mfderiv_at_unique
added theorem mdifferentiable.comp
added def mdifferentiable
added theorem mdifferentiable_at_id
added theorem mdifferentiable_chart
added theorem mdifferentiable_const
added theorem mdifferentiable_id
added theorem mdifferentiable_on_id
added def mfderiv
added theorem mfderiv_comp
added theorem mfderiv_const
added theorem mfderiv_eq_fderiv
added theorem mfderiv_id
added def mfderiv_within
added theorem mfderiv_within_comp
added theorem mfderiv_within_const
added theorem mfderiv_within_id
added theorem mfderiv_within_inter
added theorem mfderiv_within_subset
added theorem mfderiv_within_univ
added theorem unique_mdiff_on.eq
added theorem unique_mdiff_on.inter
added def unique_mdiff_on
added def ext_chart_at
added theorem ext_chart_at_source
added theorem ext_chart_at_to_inv
added theorem mem_ext_chart_source