REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: `http://hdl.handle.net/11320/4902`
 Tytuł: Stone Lattices Autorzy: Grabowski, Adam Słowa kluczowe: pseudocomplemented latticesStone latticesBoolean latticeslattice of natural divisors Data wydania: 2015 Data dodania: 16-gru-2016 Wydawca: De Gruyter Open Źródło: Formalized Mathematics, Volume 23, Issue 4, 387–396 Abstrakt: The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the paper, the notion of a pseudocomplement in a lattice is formally introduced in Mizar, and based on this we define the notion of the skeleton and the set of dense elements in a pseudocomplemented lattice, giving the meet-decomposition of arbitrary element of a lattice as the infimum of two elements: one belonging to the skeleton, and the other which is dense.The core of the paper is of course the idea of Stone identity a*⊔a**=T, which is fundamental for us: Stone lattices are those lattices L, which are distributive, bounded, and satisfy Stone identity for all elements a ∈ L. Stone algebras were introduced by Grätzer and Schmidt in [18]. Of course, the pseudocomplement is unique (if exists), so in a pseudcomplemented lattice we defined a * as the Mizar functor (unary operation mapping every element to its pseudocomplement). In Section 2 we prove formally a collection of ordinary properties of pseudocomplemented lattices.All Boolean lattices are Stone, and a natural example of the lattice which is Stone, but not Boolean, is the lattice of all natural divisors of p 2 for arbitrary prime number p (Section 6). At the end we formalize the notion of the Stone lattice B [2] (of pairs of elements a, b of B such that a ⩽ b) constructed as a sublattice of B 2, where B is arbitrary Boolean algebra (and we describe skeleton and the set of dense elements in such lattices). In a natural way, we deal with Cartesian product of pseudocomplemented lattices.Our formalization was inspired by [17], and is an important step in formalizing Jouni Järvinen Lattice theory for rough sets [19], so it follows rather the latter paper. We deal essentially with Section 4.3, pages 423–426. The description of handling complemented structures in Mizar [6] can be found in [12]. The current article together with [15] establishes the formal background for algebraic structures which are important for [10], [16] by means of mechanisms of merging theories as described in [11]. Afiliacja: Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok, Poland URI: http://hdl.handle.net/11320/4902 DOI: 10.1515/forma-2015-0031 ISSN: 1426-26301898-9934 Typ Dokumentu: Article Występuje w kolekcji(ach): Artykuły naukowe (WInf)Formalized Mathematics, 2015, Volume 23, Issue 4

Pliki w tej pozycji:
Plik Opis RozmiarFormat