Mathlib v3 is deprecated. Go to Mathlib v4

Theorem normed_space.exists_lt_norm

Modification history

2022-11-17 13:13
src/analysis/normed_space/basic.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified normed_space.exists_lt_normView on Github →
2021-12-24 00:43
src/analysis/normed_space/basic.lean
feat(analysis/normed_space): a normed space over a nondiscrete normed field is noncompact (#10994) …
Added normed_space.exists_lt_normView on Github →