with_seminorms): remove unnecessary positivity assumption (#18659)

Commit

2 years ago

chore(analysis/locally_convex/with_seminorms): remove unnecessary positivity assumption (#18659) In the boundedness definition it is not necessary to assume that the bound is positive.

Author

mcdoll

Parents

de87d505

mathlib3 b31173ee - chore(analysis/locally_convex/with_seminorms): remove unnecessary positivity assumption (#18659)

mathlib3
b31173ee - chore(analysis/locally_convex/with_seminorms): remove unnecessary positivity assumption (#18659)