Mathlib v3 is deprecated. Go to Mathlib v4

Theorem inv_norm_smul_mem_closed_unit_ball

Modification history

2022-03-26 20:22
src/analysis/normed_space/basic.lean
feat(analysis/convex/strict_convex_space): Strictly convex spaces (#11794) …
Added inv_norm_smul_mem_closed_unit_ballView on Github →