Def continuousLinearMapOfTendsto

Modification history

2026-01-16 20:13

Mathlib/Analysis/LocallyConvex/Barrelled.lean

feat: add `PolynormableSpace.banach_steinhaus` (#32481)

Added continuousLinearMapOfTendsto View on Github →

2023-08-17 21:55

Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean

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

Deleted continuousLinearMapOfTendsto View on Github →

2023-05-19 15:02

Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean

feat: port Analysis.NormedSpace.BanachSteinhaus (#4111)

Added continuousLinearMapOfTendsto View on Github →