[isabelle] Also in the AFP: Banach-Steinhaus Theorem
We are in the lucky situation of getting quite a few submissions at the moment. Is it possible that some people respond to these lockdowns by formalising mathematics? Anyway:
> We formalize is 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.
You will find it online at https://www.isa-afp.org/entries/Banach_Steinhaus.html
Many thanks to the authors for their contribution!
This archive was generated by a fusion of
Pipermail (Mailman edition) and