dual): generalize to seminormed space (#7262)

Commit

4 years ago

feat(analysis/normed_space/dual): generalize to seminormed space (#7262) We generalize here the Hahn-Banach theorem and the notion of dual space to `semi_normed_space`.

Author

riccardobrasca

Parents

700d4773

mathlib3 253d4f5b - feat(analysis/normed_space/dual): generalize to seminormed space (#7262)

mathlib3
253d4f5b - feat(analysis/normed_space/dual): generalize to seminormed space (#7262)