Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-31 11:08 09110f10

View on Github →

feat(geometry/manifold/bump_function): define smooth bump functions, baby version of the Whitney embedding thm (#6839)

  • refactor some functions in analysis/calculus/specific_functions to use bundled structures;
  • define to_euclidean, euclidean.dist, euclidean.ball, and euclidean.closed_ball;
  • define smooth bump functions on manifolds;
  • prove a baby version of the Whitney embedding theorem.

Estimated changes

deleted theorem smooth_transition.le_one
deleted theorem smooth_transition.nonneg
deleted def smooth_transition
added structure times_cont_diff_bump
added def euclidean.ball
added theorem euclidean.closure_ball
added theorem euclidean.compact_ball
added def euclidean.dist
added theorem euclidean.is_open_ball
added def to_euclidean
added structure smooth_bump_covering
added structure smooth_bump_function
added theorem smooth_at.smul
added theorem smooth_on.smul