http://hdl.handle.net/11320/13646 2026-06-01T16:16:52Z 2026-06-01T16:16:52Z Endou, Noboru http://hdl.handle.net/11320/13670 2022-07-25T08:25:01Z 2021-01-01T00:00:00Z

Tytuł: Improper Integral. Part II Autorzy: Endou, Noboru Abstrakt: In this article, using the Mizar system [2], [3], we deal with Riemann’s improper integral on infinite interval [1]. As with [4], we referred to [6], which discusses improper integrals of finite values.

2021-01-01T00:00:00Z Koch, Sebastian http://hdl.handle.net/11320/13669 2022-07-25T08:25:30Z 2021-01-01T00:00:00Z

Tytuł: About Graph Sums Autorzy: Koch, Sebastian Abstrakt: In this article the sum (or disjoint union) of graphs is formalized in the Mizar system [4], [1], based on the formalization of graphs in [9].

2021-01-01T00:00:00Z Okazaki, Hiroyuki Nakasho, Kazuhisa http://hdl.handle.net/11320/13668 2022-07-25T07:12:03Z 2021-01-01T00:00:00Z

Tytuł: The 3-Fold Product Space of Real Normed Spaces and its Properties Autorzy: Okazaki, Hiroyuki; Nakasho, Kazuhisa Abstrakt: In this article, we formalize in Mizar [1], [2] the 3-fold product space of real normed spaces for usefulness in application fields such as engineering, although the formalization of the 2-fold product space of real normed spaces has been stored in the Mizar Mathematical Library [3]. First, we prove some theorems about the 3-variable function and 3-fold Cartesian product for preparation. Then we formalize the definition of 3-fold product space of real linear spaces. Finally, we formulate the definition of 3-fold product space of real normed spaces. We referred to [7] and [6] in the formalization.

2021-01-01T00:00:00Z Schwarzweller, Christoph Rowińska-Schwarzweller, Agnieszka http://hdl.handle.net/11320/13667 2022-07-25T06:47:09Z 2021-01-01T00:00:00Z

Tytuł: Quadratic Extensions Autorzy: Schwarzweller, Christoph; Rowińska-Schwarzweller, Agnieszka Abstrakt: In this article we further develop field theory [6], [7], [12] in Mizar [1], [2], [3]: we deal with quadratic polynomials and quadratic extensions [5], [4]. First we introduce quadratic polynomials, their discriminants and prove the midnight formula. Then we show that - in case the discriminant of p being non square - adjoining a root of p’s discriminant results in a splitting field of p. Finally we prove that these are the only field extensions of degree 2, e.g. that an extension E of F is quadratic if and only if there is a non square Element a ∈ F such that E and F(√a) are isomorphic over F.

2021-01-01T00:00:00Z