http://hdl.handle.net/11320/14241 2026-06-01T17:24:49Z http://hdl.handle.net/11320/14248 Tytuł: Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces Autorzy: Nakasho, Kazuhisa; Futa, Yuichi Abstrakt: This paper formalizes in Mizar [1], [2], that the isometric isomorphisms between spaces formed by an (n + 1)-dimensional multilinear map and an n-fold composition of linear maps on real normed spaces. This result is used to describe the space of nth-order derivatives of the Frechet derivative as a multilinear space. In Section 1, we discuss the spaces of 1-dimensional multilinear maps and 0-fold compositions as a preparation, and in Section 2, we extend the discussion to the spaces of (n + 1)-dimensional multilinear map and an n-fold compositions. We referred to [4], [11], [8], [9] in this formalization. 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14247 Tytuł: Non-Trivial Universes and Sequences of Universes Autorzy: Coghetto, Roland Abstrakt: Universe is a concept which is present from the beginning of the creation of the Mizar Mathematical Library (MML) in several forms (Universe, Universe_closure, UNIVERSE) [25], then later as the_universe_of, [33], and recently with the definition GrothendieckUniverse [26], [11], [11]. These definitions are useful in many articles [28, 33, 8, 35], [19, 32, 31, 15, 6], but also [34, 12, 20, 22, 21], [27, 2, 3, 23, 16, 7, 4, 5]. In this paper, using the Mizar system [9] [10], we trivially show that Grothendieck’s definition of Universe as defined in [26], coincides with the original definition of Universe defined by Artin, Grothendieck, and Verdier (Chapitre 0 Univers et Appendice “Univers” (par N. Bourbaki) de l’Exposé I. “PREFAISCEAUX”) [1], and how the different definitions of MML concerning universes are related. We also show that the definition of Universe introduced by Mac Lane ([18]) is compatible with the MML’s definition. Although a universe may be empty, we consider the properties of non-empty universes, completing the properties proved in [25]. We introduce the notion of “trivial” and “non-trivial” Universes, depending on whether or not they contain the set ω (NAT), following the notion of Robert M. Solovay. The following result links the universes U₀ (FinSETS) and U₁ (SETS): GrothendieckUniverse ω = GrothendieckUniverse U₀ = U₁ . Before turning to the last section, we establish some trivial propositions allowing the construction of sets outside the considered universe. The last section is devoted to the construction, in Tarski-Grothendieck, of a tower of universes indexed by the ordinal numbers (See 8. Examples, Grothendieck universe, ncatlab.org [24]). Grothendieck’s universe is referenced in current works: “Assuming the existence of a sufficient supply of (Grothendieck) univers”, Jacob Lurie in “Higher Topos Theory” [17], “Annexe B – Some results on Grothendieck universes”, Olivia Caramello and Riccardo Zanfa in “Relative topos theory via stacks” [13], “Remark 1.1.5 (quoting Michael Shulman [30])”, Emily Riehl in “Category the ory in Context” [29], and more specifically “Strict Universes for Grothendieck Topoi” [14]. 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14245 Tytuł: Absolutely Integrable Functions Autorzy: Endou, Noboru Abstrakt: The goal of this article is to clarify the relationship between Riemann’s improper integrals and Lebesgue integrals. In previous articles [6], [7], we treated Riemann’s improper integrals [1], [11] and [4] on arbitrary intervals. Therefore, in this article, we will continue to clarify the relationship between improper integrals and Lebesgue integrals [8], using the Mizar [3], [2] formalism. 2022-01-01T00:00:00Z http://hdl.handle.net/11320/14244 Tytuł: Splitting Fields for the Rational Polynomials X²−2, X²+X+1, X³−1, and X³−2 Autorzy: Schwarzweller, Christoph; Burgoa, Sara Abstrakt: In [11] the existence (and uniqueness) of splitting fields has been formalized. In this article we apply this result by providing splitting fields for the polynomials X² − 2, X³ − 1, X² + X + 1 and X³ − 2 over Q using the Mizar [2], [1] formalism. We also compute the degrees and bases for these splitting fields, which requires some additional registrations to adopt types properly. The main result, however, is that the polynomial X³ − 2 does not split over Q(∛2). Because X³ − 2 obviously has a root over Q(∛2), this shows that the field extension Q(∛2) is not normal over Q [3], [4], [5] and [7]. 2022-01-01T00:00:00Z