DSpace Kolekcja:http://hdl.handle.net/11320/36622020-05-30T06:35:29Z2020-05-30T06:35:29ZIsomorphisms of Direct Products of Cyclic Groups of Prime Power OrderYamazaki, HiroshiOkazaki, HiroyukiNakasho, KazuhisaShidama, Yasunarihttp://hdl.handle.net/11320/36892017-10-05T22:56:46Z2013-01-01T00:00:00ZTytuł: Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order
Autorzy: Yamazaki, Hiroshi; Okazaki, Hiroyuki; Nakasho, Kazuhisa; Shidama, Yasunari
Abstrakt: In this paper we formalized some theorems concerning the cyclic groups of prime power order. We formalize that every commutative cyclic group of prime power order is isomorphic to a direct product of family of cyclic groups [1], [18].2013-01-01T00:00:00ZPrime Filters and Ideals in Distributive LatticesGrabowski, Adamhttp://hdl.handle.net/11320/36902017-10-05T22:56:47Z2013-01-01T00:00:00ZTytuł: Prime Filters and Ideals in Distributive Lattices
Autorzy: Grabowski, Adam
Abstrakt: The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar Mathematical Library, there are some attempts to formalize prime ideals and filters; one series of articles written as decoding [9] proven some results; we tried however to follow [21], [12], and [13]. All three were devoted to the Stone representation theorem [18] for Boolean or Heyting lattices. The main aim of the present article was to bridge this gap between general distributive lattices and Boolean algebras, having in mind that the more general approach will eventually replace the common proof of aforementioned articles.1
Because in Boolean algebras the notions of ultrafilters, prime filters and maximal filters coincide, we decided to construct some concrete examples of ultrafilters in nontrivial Boolean lattice. We proved also the Prime Ideal Theorem not as BPI (Boolean Prime Ideal), but in the more general setting.
In the final section we present Nachbin theorems [15],[1] expressed both in terms of maximal and prime filters and as the unordered spectra of a lattice [11], [10]. This shows that if the notion of maximal and prime filters coincide in the lattice, it is Boolean.2013-01-01T00:00:00ZIntroduction to Formal Preference SpacesNiewiadomska, ElizaGrabowski, Adamhttp://hdl.handle.net/11320/36912017-10-05T22:57:30Z2013-01-01T00:00:00ZTytuł: Introduction to Formal Preference Spaces
Autorzy: Niewiadomska, Eliza; Grabowski, Adam
Abstrakt: In the article the formal characterization of preference spaces [1] is given. As the preference relation is one of the very basic notions of mathematical economics [9], it prepares some ground for a more thorough formalization of consumer theory (although some work has already been done - see [17]). There was an attempt to formalize similar results in Mizar, but this work seems still unfinished [18].
There are many approaches to preferences in literature. We modelled them in a rather illustrative way (similar structures were considered in [8]): either the consumer (strictly) prefers an alternative, or they are of equal interest; he/she could also have no opinion of the choice. Then our structures are based on three relations on the (arbitrary, not necessarily finite) set of alternatives. The completeness property can however also be modelled, although we rather follow [2] which is more general [12]. Additionally we assume all three relations are disjoint and their set-theoretic union gives a whole universe of alternatives.
We constructed some positive and negative examples of preference structures; the main aim of the article however is to give the characterization of consumer preference structures in terms of a binary relation, called characteristic relation [10], and to show the way the corresponding structure can be obtained only using this relation. Finally, we show the connection between tournament and total spaces and usual properties of the ordering relations.2013-01-01T00:00:00ZThe Linearity of Riemann Integral on Functions from R into Real Banach SpaceNarita, KeikoEndou, NoboruShidama, Yasunarihttp://hdl.handle.net/11320/36872017-10-05T22:57:37Z2013-01-01T00:00:00ZTytuł: The Linearity of Riemann Integral on Functions from R into Real Banach Space
Autorzy: Narita, Keiko; Endou, Noboru; Shidama, Yasunari
Abstrakt: In this article, we described basic properties of Riemann integral on functions from R into Real Banach Space. We proved mainly the linearity of integral operator about the integral of continuous functions on closed interval of the set of real numbers. These theorems were based on the article [10] and we referred to the former articles about Riemann integral. We applied definitions and theorems introduced in the article [9] and the article [11] to the proof. Using the definition of the article [10], we also proved some theorems on bounded functions.2013-01-01T00:00:00Z