Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Sakurai, Hideki, Okazaki, Hiroyuki, Shidama, Yasunari
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Nakasho, Kazuhisa, Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
N-Dimensional Binary Vector Spaces
Arai, Kenichi, Okazaki, Hiroyuki
Isomorphisms of Direct Products of Finite Cyclic Groups
Arai, Kenichi, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Double Sequences and Limits
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Integral Linear Space
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi
More on Continuous Functions on Normed Linear Spaces
Okazaki, Hiroyuki, Endou, Noboru, Shidama, Yasunari
Real Vector Space and Related Notions
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari