http://hdl.handle.net/11320/7593 2026-06-01T07:20:34Z http://hdl.handle.net/11320/7632 Tytuł: Continuity of Bounded Linear Operators on Normed Linear Spaces Autorzy: Nakasho, Kazuhisa; Futa, Yuichi; Shidama, Yasunari Abstrakt: 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. 2018-01-01T00:00:00Z http://hdl.handle.net/11320/7630 Tytuł: Some Remarks about Product Spaces Autorzy: Koch, Sebastian Abstrakt: This article covers some technical aspects about the product topology which are usually not given much of a thought in mathematics and standard literature like [7] and [6], not even by Bourbaki in [4]. Let {Ti}i∈I be a family of topological spaces. The prebasis of the product space T =Qi∈ITi is defined in [5] as the set of all π−1i(V ) with i ∈ I and V open in Ti. Here it is shown that the basis generated by this prebasis consists exactly of the sets Qi∈IVi with Vi open in Ti and for all but finitely many i ∈ I holds Vi = Ti. Given I = {a} we have T ∼= Ta, given I = {a, b} with a 6= b we have T ∼= Ta × Tb. Given another family of topological spaces {Si}i∈I such that Si ∼= Ti for all i ∈ I, we have S = Qi∈ISi ∼= T . If instead Si is a subspace of Ti for each i ∈ I, then S is a subspace of T . These results are obvious for mathematicians, but formally proven here by means of the Mizar system [3], [2]. 2018-01-01T00:00:00Z http://hdl.handle.net/11320/7631 Tytuł: Binary Representation of Natural Numbers Autorzy: Okazaki, Hiroyuki Abstrakt: Binary representation of integers [5], [3] and arithmetic operations on them have already been introduced in Mizar Mathematical Library [8, 7, 6, 4]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values.In this article we formalize, by means of Mizar system [2], [1], the binary representation of natural numbers which maps ℕ into bitstreams. Opis: This study was supported in part by JSPS KAKENHI Grant Numbers JP17K00182. The author would also like to express gratitude to Prof. Yasunari Shidama for his support and encouragement. 2018-01-01T00:00:00Z http://hdl.handle.net/11320/7629 Tytuł: Arithmetic Operations on Short Finite Sequences Autorzy: Ziobro, Rafał Abstrakt: In contrast to other proving systems Mizar Mathematical Library, considered as one of the largest formal mathematical libraries [4], is maintained as a single base of theorems, which allows the users to benefit from earlier formalized items [3], [2]. This eventually leads to a development of certain branches of articles using common notation and ideas. Such formalism for finite sequences has been developed since 1989 [1] and further developed despite of the controversy over indexing which excludes zero [6], also for some advanced and new mathematics [5].The article aims to add some new machinery for dealing with finite sequences, especially those of short length. 2018-01-01T00:00:00Z