Banach-Steinhaus Theorem (Q7361773)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Banach_Steinhaus
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Banach-Steinhaus Theorem |
AFP entry Banach_Steinhaus |
Statements
2 May 2020
0 references
Dominique Unruh
0 references
José Manuel Rodríguez Caballero
0 references
Banach-Steinhaus Theorem (English)
0 references
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.
0 references
