Commit 2026-01-16 20:13 ebafbffb

View on Github →

feat: add PolynormableSpace.banach_steinhaus (#32481)

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

added def continuousLinearMapOfTendsto

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

added theorem WithSeminorms.isVonNBounded_iff_seminorm_bddAbove

Modified Mathlib/Analysis/Normed/Operator/BanachSteinhaus.lean