Mathlib v3 is deprecated. Go to Mathlib v4

Def homeomorph_unit_ball

Modification history

2022-12-12 09:04
src/analysis/normed_space/basic.lean
fix(analysis/normed_space/basic): add back computable module instance (#17813) …
Deleted homeomorph_unit_ballView on Github →
2022-08-15 09:04
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/basic): change `homeomorph_unit_ball` to make it obviously smooth (#15980) …
Modified homeomorph_unit_ballView on Github →
2022-07-24 16:34
src/analysis/normed_space/basic.lean
chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) …
Modified homeomorph_unit_ballView on Github →
2022-01-16 13:30
src/analysis/normed_space/basic.lean
refactor(analysis/normed_space): merge `normed_space` and `semi_normed_space` (#8218) …
Modified homeomorph_unit_ballView on Github →
2021-12-11 11:06
src/analysis/normed_space/basic.lean
feat(analysis/normed_space): normed space is homeomorphic to the unit ball (#10690)
Added homeomorph_unit_ballView on Github →