DSpace Kolekcja: http://hdl.handle.net/11320/3579 Mon, 01 Jun 2026 07:20:39 GMT 2026-06-01T07:20:39Z More on Continuous Functions on Normed Linear Spaces http://hdl.handle.net/11320/3595 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]. Sat, 01 Jan 2011 00:00:00 GMT http://hdl.handle.net/11320/3595 2011-01-01T00:00:00Z Cartesian Products of Family of Real Linear Spaces http://hdl.handle.net/11320/3596 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. Sat, 01 Jan 2011 00:00:00 GMT http://hdl.handle.net/11320/3596 2011-01-01T00:00:00Z Formalization of Integral Linear Space http://hdl.handle.net/11320/3597 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]. Sat, 01 Jan 2011 00:00:00 GMT http://hdl.handle.net/11320/3597 2011-01-01T00:00:00Z Normal Subgroup of Product of Groups http://hdl.handle.net/11320/3591 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. Sat, 01 Jan 2011 00:00:00 GMT http://hdl.handle.net/11320/3591 2011-01-01T00:00:00Z