Theorem WithSeminorms.topologicalSpace_eq_iInf

Modification history

2026-09-29 15:02
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
feat: introduce an IsNormableSpace class (#42983) …
Added WithSeminorms.topologicalSpace_eq_iInfView on Github →