Commit 2023-08-17 21:55 32744871

View on Github →

feat(Analysis.LocallyConvex.Barrelled): generalize Banach-Steinhaus theorem (#5676)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/LocallyConvex/Barrelled.lean

added theorem Seminorm.continuous_iSup

added theorem Seminorm.continuous_of_lowerSemicontinuous

Modified Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean

deleted def continuousLinearMapOfTendsto