Structure WithSeminorms

Modification history

2023-07-12 09:20
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
feat(Analysis.LocallyConvex.WithSeminorms): `WithSeminorms` for infimum of topologies (#5816)
Modified WithSeminormsView on Github →
2023-05-24 09:57
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
feat: port Analysis.LocallyConvex.WithSeminorms (#4170)
Added WithSeminormsView on Github →