Theorem Seminorm.continuous_of_lowerSemicontinuous

Modification history

2023-08-17 21:55
Mathlib/Analysis/LocallyConvex/Barrelled.lean
feat(Analysis.LocallyConvex.Barrelled): generalize Banach-Steinhaus theorem (#5676)
Added Seminorm.continuous_of_lowerSemicontinuousView on Github →