DSpace Kolekcja: http://hdl.handle.net/11320/3579 2026-06-01T07:20:39Z 2026-06-01T07:20:39Z More on Continuous Functions on Normed Linear Spaces Okazaki, Hiroyuki Endou, Noboru Shidama, Yasunari http://hdl.handle.net/11320/3595 2017-10-05T22:57:19Z 2011-01-01T00:00:00Z Tytuł: More on Continuous Functions on Normed Linear Spaces Autorzy: Okazaki, Hiroyuki; Endou, Noboru; Shidama, Yasunari Abstrakt: In this article we formalize the definition and some facts about continuous functions from R into normed linear spaces [14]. 2011-01-01T00:00:00Z Cartesian Products of Family of Real Linear Spaces Okazaki, Hiroyuki Endou, Noboru Shidama, Yasunari http://hdl.handle.net/11320/3596 2017-10-05T22:55:02Z 2011-01-01T00:00:00Z Tytuł: Cartesian Products of Family of Real Linear Spaces Autorzy: Okazaki, Hiroyuki; Endou, Noboru; Shidama, Yasunari Abstrakt: In this article we introduced the isomorphism mapping between cartesian products of family of linear spaces [4]. Those products had been formalized by two different ways, i.e., the way using the functor [:X, Y:] and ones using the functor "product". By the same way, the isomorphism mapping was defined between Cartesian products of family of linear normed spaces also. 2011-01-01T00:00:00Z Formalization of Integral Linear Space Futa, Yuichi Okazaki, Hiroyuki Shidama, Yasunari http://hdl.handle.net/11320/3597 2017-10-05T22:55:03Z 2011-01-01T00:00:00Z Tytuł: Formalization of Integral Linear Space Autorzy: Futa, Yuichi; Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: In this article, we formalize integral linear spaces, that is a linear space with integer coefficients. Integral linear spaces are necessary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm that outputs short lattice base and cryptographic systems with lattice [8]. 2011-01-01T00:00:00Z Normal Subgroup of Product of Groups Okazaki, Hiroyuki Arai, Kenichi Shidama, Yasunari http://hdl.handle.net/11320/3591 2017-10-05T22:54:36Z 2011-01-01T00:00:00Z Tytuł: Normal Subgroup of Product of Groups Autorzy: Okazaki, Hiroyuki; Arai, Kenichi; Shidama, Yasunari Abstrakt: In [6] it was formalized that the direct product of a family of groups gives a new group. In this article, we formalize that for all j ∈ I, the group G = Πi∈IGi has a normal subgroup isomorphic to Gj. Moreover, we show some relations between a family of groups and its direct product. 2011-01-01T00:00:00Z