Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-23 23:11 e2a8e639

View on Github →

feat(geometry/manifold): improvements for smooth manifolds (#1593)

  • feat(geometry/manifold): improvements to smooth manifolds
  • fix
  • better definition for half-space
  • fix docstring
  • address comments
  • more comments

Estimated changes

added theorem times_cont_diff.add
added theorem times_cont_diff.neg
added theorem times_cont_diff.sub
added theorem times_cont_diff_on.add
added theorem times_cont_diff_on.neg
added theorem times_cont_diff_on.sub
added def Icc_left_chart
added def Icc_right_chart
added def euclidean_space
added theorem findim_euclidean_space
added def lt_class
added theorem range_half_space
added theorem range_quadrant
deleted def euclidean_space
deleted theorem range_half_space
modified theorem times_cont_diff_groupoid_le