with_seminorms): the topology induced by a family of seminorms is the infimum of the ones induced by each seminorm (#16669)

Commit

3 years ago

feat(analysis/locally_convex/with_seminorms): the topology induced by a family of seminorms is the infimum of the ones induced by each seminorm (#16669) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author

ADedecker

Parents

348289cc

mathlib3 c80bc30e - feat(analysis/locally_convex/with_seminorms): the topology induced by a family of seminorms is the infimum of the ones induced by each seminorm (#16669)

mathlib3
c80bc30e - feat(analysis/locally_convex/with_seminorms): the topology induced by a family of seminorms is the infimum of the ones induced by each seminorm (#16669)