### 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.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Banach_Steinhaus

- Banach_Steinhaus_Missing
- Banach_Steinhaus

### Used by

- Complex Bounded Operators

## Cite

×

Banach_Steinhaus-AFP

    @article{Banach_Steinhaus-AFP,
      author  = {Dominique Unruh and José Manuel Rodríguez Caballero},
      title   = {Banach-Steinhaus Theorem},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Banach_Steinhaus.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- May 11, 2020 : Isabelle2020
- May 6, 2020 : Isabelle2020