basic): add `normed_space.unbounded_univ` (#11131)

Commit

4 years ago

chore(analysis/normed_space/basic): add `normed_space.unbounded_univ` (#11131) Extract it from the proof of `normed_space.noncompact_space`.

Author

urkud

Parents