Theorem withSeminorms_iInf

Modification history

2023-08-10 19:52
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified withSeminorms_iInfView on Github →
2023-07-12 09:20
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
feat(Analysis.LocallyConvex.WithSeminorms): `WithSeminorms` for infimum of topologies (#5816)
Added withSeminorms_iInfView on Github →