Commit 2021-12-31 22:23 200f47d3

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.

• depends on: #10700