Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cont_diff_on_homeomorph_unit_ball_symm

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_on_homeomorph_unit_ball_symmView on Github →