http://hdl.handle.net/11320/4799 Mon, 01 Jun 2026 19:17:44 GMT 2026-06-01T19:17:44Z http://hdl.handle.net/11320/4899 Tytuł: Extended Real-Valued Double Sequence and Its Convergence Autorzy: Endou, Noboru Abstrakt: AbstractIn this article we introduce the convergence of extended realvalued double sequences [16], [17]. It is similar to our previous articles [15], [10]. In addition, we also prove Fatou’s lemma and the monotone convergence theorem for double sequences. Thu, 01 Jan 2015 00:00:00 GMT http://hdl.handle.net/11320/4899 2015-01-01T00:00:00Z http://hdl.handle.net/11320/4898 Tytuł: The Orthogonal Projection and the Riesz Representation Theorem Autorzy: Narita, Keiko; Endou, Noboru; Shidama, Yasunari Abstrakt: AbstractIn this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals on real Hilbert spaces. Referring to the article [15], we also defined some definitions on real Hilbert spaces and proved some theorems for defining dual spaces of real Hilbert spaces. As to the properties of all definitions, we proved that they are equivalent properties of functionals on real normed spaces. In Sec. 2, by the definitions [11], we showed properties of the orthogonal complement. Then we proved theorems on the orthogonal decomposition of elements of real Hilbert spaces. They are the last two theorems of existence and uniqueness. In the third and final section, we defined the kernel of linear functionals on real Hilbert spaces. By the last three theorems, we showed the Riesz representation theorem, existence, uniqueness, and the property of the norm of bounded linear functionals on real Hilbert spaces. We referred to [36], [9], [24] and [3] in the formalization. Thu, 01 Jan 2015 00:00:00 GMT http://hdl.handle.net/11320/4898 2015-01-01T00:00:00Z http://hdl.handle.net/11320/4894 Tytuł: Convergent Filter Bases Autorzy: Coghetto, Roland Abstrakt: AbstractWe are inspired by the work of Henri Cartan [16], Bourbaki [10] (TG. I Filtres) and Claude Wagschal [34]. We define the base of filter, image filter, convergent filter bases, limit filter and the filter base of tails (fr: filtre des sections). Thu, 01 Jan 2015 00:00:00 GMT http://hdl.handle.net/11320/4894 2015-01-01T00:00:00Z http://hdl.handle.net/11320/4896 Tytuł: Fermat’s Little Theorem via Divisibility of Newton’s Binomial Autorzy: Ziobro, Rafał Abstrakt: AbstractSolving equations in integers is an important part of the number theory [29]. In many cases it can be conducted by the factorization of equation’s elements, such as the Newton’s binomial. The article introduces several simple formulas, which may facilitate this process. Some of them are taken from relevant books [28], [14]. In the second section of the article, Fermat’s Little Theorem is proved in a classical way, on the basis of divisibility of Newton’s binomial. Although slightly redundant in its content (another proof of the theorem has earlier been included in [12]), the article provides a good example, how the application of registrations could shorten the length of Mizar proofs [9], [17]. Thu, 01 Jan 2015 00:00:00 GMT http://hdl.handle.net/11320/4896 2015-01-01T00:00:00Z