mathlib
573ca836 - feat(analysis/seminorm): add some lemmas for seminorm balls (#11471)

Commit

3 years ago

feat(analysis/seminorm): add some lemmas for seminorm balls (#11471) Add some lemmas for seminorm balls. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

mcdoll

Parents

07d8ca6d

mathlib 573ca836 - feat(analysis/seminorm): add some lemmas for seminorm balls (#11471)

mathlib
573ca836 - feat(analysis/seminorm): add some lemmas for seminorm balls (#11471)