mathlib

200f47d3 - feat(analysis/normed_space/banach_steinhaus): prove the standard Banach-Steinhaus theorem (#10663)

feat(analysis/normed_space/banach_steinhaus): prove the standard Banach-Steinhaus theorem (#10663) Here we prove the Banach-Steinhaus theorem for maps from a Banach space into a (semi-)normed space. This is the standard version of the theorem and the proof proceeds via the Baire category theorem. Notably, the version from barelled spaces to locally convex spaces is not included because these spaces do not yet exist in `mathlib`. In addition, it is established that the pointwise limit of continuous linear maps from a Banach space into a normed space is itself a continuous linear map. - [x] depends on: #10700 Co-authored-by: Patrick Massot <patrickmassot@free.fr>