DSpace Kolekcja:
http://hdl.handle.net/11320/4797
Mon, 30 Nov 2020 19:22:05 GMT2020-11-30T19:22:05Zσ-ring and σ-algebra of Sets
http://hdl.handle.net/11320/4837
Tytuł: σ-ring and σ-algebra of Sets
Autorzy: Endou, Noboru; Nakasho, Kazuhisa; Shidama, Yasunari
Abstrakt: In this article, semiring and semialgebra of sets are formalized so as to construct a measure of a given set in the next step. Although a semiring of sets has already been formalized in [13], that is, strictly speaking, a definition of a quasi semiring of sets suggested in the last few decades [15]. We adopt a classical definition of a semiring of sets here to avoid such a confusion. Ring of sets and algebra of sets have been formalized as non empty preboolean set [23] and field of subsets [18], respectively. In the second section, definitions of a ring and a σ-ring of sets, which are based on a semiring and a ring of sets respectively, are formalized and their related theorems are proved. In the third section, definitions of an algebra and a σ-algebra of sets, which are based on a semialgebra and an algebra of sets respectively, are formalized and their related theorems are proved. In the last section, mutual relationships between σ-ring and σ-algebra of sets are formalized and some related examples are given. The formalization is based on [15], and also referred to [9] and [16].Thu, 01 Jan 2015 00:00:00 GMThttp://hdl.handle.net/11320/48372015-01-01T00:00:00ZDefinition and Properties of Direct Sum Decomposition of Groups
http://hdl.handle.net/11320/4835
Tytuł: Definition and Properties of Direct Sum Decomposition of Groups
Autorzy: Nakasho, Kazuhisa; Yamazaki, Hiroshi; Okazaki, Hiroyuki; Shidama, Yasunari
Abstrakt: In this article, direct sum decomposition of group is mainly discussed. In the second section, support of element of direct product group is defined and its properties are formalized. It is formalized here that an element of direct product group belongs to its direct sum if and only if support of the element is finite. In the third section, product map and sum map are prepared. In the fourth section, internal and external direct sum are defined. In the last section, an equivalent form of internal direct sum is proved. We referred to [23], [22], [8] and [18] in the formalization.Thu, 01 Jan 2015 00:00:00 GMThttp://hdl.handle.net/11320/48352015-01-01T00:00:00ZSeparability of Real Normed Spaces and Its Basic Properties
http://hdl.handle.net/11320/4838
Tytuł: Separability of Real Normed Spaces and Its Basic Properties
Autorzy: Nakasho, Kazuhisa; Endou, Noboru
Abstrakt: In this article, the separability of real normed spaces and its properties are mainly formalized. In the first section, it is proved that a real normed subspace is separable if it is generated by a countable subset. We used here the fact that the rational numbers form a dense subset of the real numbers. In the second section, the basic properties of the separable normed spaces are discussed. It is applied to isomorphic spaces via bounded linear operators and double dual spaces. In the last section, it is proved that the completeness and reflexivity are transferred to sublinear normed spaces. The formalization is based on [34], and also referred to [7], [14] and [16].Thu, 01 Jan 2015 00:00:00 GMThttp://hdl.handle.net/11320/48382015-01-01T00:00:00ZCategorical Pullbacks
http://hdl.handle.net/11320/4834
Tytuł: Categorical Pullbacks
Autorzy: Riccardi, Marco
Abstrakt: The main purpose of this article is to introduce the categorical concept of pullback in Mizar. In the first part of this article we redefine homsets, monomorphisms, epimorpshisms and isomorphisms [7] within a free-object category [1] and it is shown there that ordinal numbers can be considered as categories. Then the pullback is introduced in terms of its universal property and the Pullback Lemma is formalized [15]. In the last part of the article we formalize the pullback of functors [14] and it is also shown that it is not possible to write an equivalent definition in the context of the previous Mizar formalization of category theory [8].Thu, 01 Jan 2015 00:00:00 GMThttp://hdl.handle.net/11320/48342015-01-01T00:00:00Z