<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, using the Mizar system <xref ref-type="bibr" rid="j_forma-2018-0021_ref_001_w2aab3b7b3b1b6b1ab1ab1Aa">[1]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0021_ref_002_w2aab3b7b3b1b6b1ab1ab2Aa">[2]</xref>, 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.</p><p>In the last section, we formalized that continuity of bilinear operator is equivalent to both Lipschitz continuity and local continuity. We referred to <xref ref-type="bibr" rid="j_forma-2018-0021_ref_004_w2aab3b7b3b1b6b1ab1ab4Aa">[4]</xref>, <xref ref-type="bibr" rid="j_forma-2018-0021_ref_013_w2aab3b7b3b1b6b1ab1ac13Aa">[13]</xref>, and <xref ref-type="bibr" rid="j_forma-2018-0021_ref_003_w2aab3b7b3b1b6b1ab1ab3Aa">[3]</xref> in this formalization.</p></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.

Continuity of Bounded Linear Operators on Normed Linear Spaces

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Continuity of Bounded Linear Operators on Normed Linear Spaces"}

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

Continuity of Bounded Linear Operators on Normed Linear Spaces

Data publikacji: 23 lut 2019

Zakres stron: 231 - 237

Przyjęty: 29 wrz 2018

DOI: https://doi.org/10.2478/forma-2018-0021

Słowa kluczowe
Lipschitz continuity, uniform continuity, bounded linear operators, bilinear operators

© 2018 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Continuity of Bounded Linear Operators on Normed Linear Spaces

Data publikacji: 23 lut 2019

Zakres stron: 231 - 237

Przyjęty: 29 wrz 2018

DOI: https://doi.org/10.2478/forma-2018-0021

Słowa kluczoweLipschitz continuity, uniform continuity, bounded linear operators, bilinear operators

© 2018 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Słowa kluczowe
Lipschitz continuity, uniform continuity, bounded linear operators, bilinear operators