REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: `http://hdl.handle.net/11320/3690`
 Tytuł: Prime Filters and Ideals in Distributive Lattices Autorzy: Grabowski, Adam Słowa kluczowe: prime filtersprime idealsdistributive lattices Data wydania: 2013 Data dodania: 9-gru-2015 Wydawca: De Gruyter Open Źródło: Formalized Mathematics, Volume 21, Issue 3, 2013, Pages 213-221 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. Afiliacja: Institute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland URI: http://hdl.handle.net/11320/3690 DOI: 10.2478/forma-2013-0023 ISSN: 1426-26301898-9934 Typ Dokumentu: Article Występuje w kolekcji(ach): Artykuły naukowe (WMiI)Formalized Mathematics, 2013, Volume 21, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat