# Banach-Steinhaus Theorem

 Title: Banach-Steinhaus Theorem Authors: Dominique Unruh and Jose Manuel Rodriguez Caballero Submission date: 2020-05-02 Abstract: We formalize in Isabelle/HOL a result due to S. Banach and H. Steinhaus known as the Banach-Steinhaus theorem or Uniform boundedness principle: a pointwise-bounded family of continuous linear operators from a Banach space to a normed space is uniformly bounded. Our approach is an adaptation to Isabelle/HOL of a proof due to A. Sokal. BibTeX: @article{Banach_Steinhaus-AFP, author = {Dominique Unruh and Jose Manuel Rodriguez Caballero}, title = {Banach-Steinhaus Theorem}, journal = {Archive of Formal Proofs}, month = may, year = 2020, note = {\url{http://isa-afp.org/entries/Banach_Steinhaus.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License