Commit 2022-08-15 09:04 4a379da7

View on Github →

feat(analysis/normed_space/basic): change homeomorph_unit_ball to make it obviously smooth (#15980) Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/analysis/inner_product_space/calculus.lean

added theorem cont_diff_homeomorph_unit_ball

added theorem cont_diff_on_homeomorph_unit_ball_symm

Modified src/analysis/normed_space/basic.lean

added theorem coe_homeomorph_unit_ball_apply_zero

modified def homeomorph_unit_ball