Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cont_diff_homeomorph_unit_ball

Modification history

2022-08-15 09:04
src/analysis/inner_product_space/calculus.lean
feat(analysis/normed_space/basic): change `homeomorph_unit_ball` to make it obviously smooth (#15980) …
Added cont_diff_homeomorph_unit_ballView on Github →