Commit 2023-05-19 15:02 a0e77e7f

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/BanachSteinhaus.lean

added theorem banach_steinhaus

added theorem banach_steinhaus_iSup_nnnorm

added def continuousLinearMapOfTendsto