Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Tytuł: Stone Lattices
Autorzy: Grabowski, Adam
Słowa kluczowe: pseudocomplemented lattices
Stone lattices
Boolean lattices
lattice 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
DOI: 10.1515/forma-2015-0031
ISSN: 1426-2630
Typ Dokumentu: Article
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2015, Volume 23, Issue 4

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2015-0031.pdf280,64 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons