[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!

Larry





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.