lp_space): API for `lp.single` (#11307)

Commit

4 years ago

feat(analysis/normed_space/lp_space): API for `lp.single` (#11307) Definition and basic properties for `lp.single`, an element of `lp` space supported at one point.

Author

hrmacbeth

Parents

cdd44cd7

mathlib af074c84 - feat(analysis/normed_space/lp_space): API for `lp.single` (#11307)

mathlib
af074c84 - feat(analysis/normed_space/lp_space): API for `lp.single` (#11307)