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].
@article{bwmeta1.element.doi-10_1515_forma-2015-0031,
author = {Adam Grabowski},
title = {Stone Lattices},
journal = {Formalized Mathematics},
volume = {23},
year = {2015},
pages = {387-396},
zbl = {1339.06009},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2015-0031}
}
Adam Grabowski. Stone Lattices. Formalized Mathematics, Tome 23 (2015) pp. 387-396. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2015-0031/
[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.
[2] Grzegorz Bancerek. Filters – part II. Quotient lattices modulo filters and direct product of two lattices. Formalized Mathematics, 2(3):433–438, 1991.
[3] Grzegorz Bancerek. Ideals. Formalized Mathematics, 5(2):149–156, 1996.
[4] Grzegorz Bancerek. Complete lattices. Formalized Mathematics, 2(5):719–725, 1991.
[5] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.
[6] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8 17.[Crossref] | Zbl 06512423
[7] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.
[8] Marek Chmur. The lattice of natural numbers and the sublattice of it. The set of prime numbers. Formalized Mathematics, 2(4):453–459, 1991.
[9] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.
[10] Adam Grabowski. On the computer-assisted reasoning about rough sets. In B. Dunin-Kęplicz, A. Jankowski, A. Skowron, and M. Szczuka, editors, International Workshop on Monitoring, Security, and Rescue Techniques in Multiagent Systems Location, volume 28 of Advances in Soft Computing, pages 215–226, Berlin, Heidelberg, 2005. Springer-Verlag. doi:10.1007/3-540-32370-8 15.[Crossref] | Zbl 1090.68574
[11] Adam Grabowski. Efficient rough set theory merging. Fundamenta Informaticae, 135(4): 371–385, 2014. doi:10.3233/FI-2014-1129.[Crossref][WoS] | Zbl 1329.68247
[12] Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211–221, 2015. doi:10.1007/s10817-015-9333-5.[Crossref] | Zbl 06585255
[13] Adam Grabowski. Prime filters and ideals in distributive lattices. Formalized Mathematics, 21(3):213–221, 2013. doi:10.2478/forma-2013-0023.[Crossref] | Zbl 1298.06003
[14] Adam Grabowski. On square-free numbers. Formalized Mathematics, 21(2):153–162, 2013. doi:10.2478/forma-2013-0017.[Crossref] | Zbl 1298.11008
[15] Adam Grabowski. Two axiomatizations of Nelson algebras. Formalized Mathematics, 23 (2):115–125, 2015. doi:10.1515/forma-2015-0012.[Crossref] | Zbl 1318.06010
[16] Adam Grabowski and Magdalena Jastrzębska. Rough set theory from a math-assistant perspective. In Rough Sets and Intelligent Systems Paradigms, International Conference, RSEISP 2007, Warsaw, Poland, June 28–30, 2007, Proceedings, pages 152–161, 2007. doi:10.1007/978-3-540-73451-2 17.[Crossref]
[17] George Grätzer. Lattice Theory: Foundation. Birkhäuser, 2011. | Zbl 1233.06001
[18] George Grätzer and E.T. Schmidt. On a problem of M.H. Stone. Acta Mathematica Academiae Scientarum Hungaricae, (8):455–460, 1957.
[19] Jouni Järvinen. Lattice theory for rough sets. Transactions of Rough Sets, VI, Lecture Notes in Computer Science, 4374:400–498, 2007. | Zbl 1186.03069
[20] Magdalena Jastrzębska and Adam Grabowski. On the properties of the Möbius function. Formalized Mathematics, 14(1):29–36, 2006. doi:10.2478/v10037-006-0005-0.[Crossref]
[21] Jolanta Kamieńska and Jarosław Stanisław Walijewski. Homomorphisms of lattices, finite join and finite meet. Formalized Mathematics, 4(1):35–40, 1993.
[22] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990.
[23] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829–832, 1990.
[24] Robert Milewski. More on the lattice of many sorted equivalence relations. Formalized Mathematics, 5(4):565–569, 1996.
[25] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990.
[26] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.
[27] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.
[28] Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215–222, 1990.