Name
Abstract | ||
|---|---|---|
In this article, using the Mizar system [1], [2], we discuss the continuity of bounded linear operators on normed linear spaces. In the first section, it is discussed that bounded linear operators on normed linear spaces are uniformly continuous and Lipschitz continuous. Especially, a bounded linear operator on the dense subset of a complete normed linear space has a unique natural extension over the whole space. In the next section, several basic currying properties are formalized. In the last section, we formalized that continuity of bilinear operator is equivalent to both Lipschitz continuity and local continuity. We referred to [4], [13], and [3] in this formalization. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.2478/forma-2018-0021 | FORMALIZED MATHEMATICS |
Keywords | Field | DocType |
Lipschitz continuity,uniform continuity,bounded linear operators,bilinear operators | Discrete mathematics,Pure mathematics,Uniform continuity,Lipschitz continuity,Operator (computer programming),Mathematics,Bounded function | Journal |
Volume | Issue | ISSN |
26 | 3 | 1898-9934 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kazuhisa Nakasho | 1 | 7 | 8.59 |
| Yuichi Futa | 2 | 23 | 15.08 |
| Yasunari Shidama | 3 | 166 | 72.47 |