DSpace Kolekcja:
http://hdl.handle.net/11320/3579
2024-11-06T04:38:00ZFormalization 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].2011-01-01T00:00:00ZCartesian 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.2011-01-01T00:00:00ZMore 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].2011-01-01T00:00:00ZThe Definition of Topological Manifolds
http://hdl.handle.net/11320/3594
Tytuł: The Definition of Topological Manifolds
Autorzy: Riccardi, Marco
Abstrakt: This article introduces the definition of n-locally Euclidean topological spaces and topological manifolds [13].2011-01-01T00:00:00Z