Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Also in the AFP: Banach-Steinhaus Theorem

Email Gateway (Aug 23 2022 at 09:04):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

Last updated: Apr 24 2024 at 20:16 UTC