:: Stone Lattices
:: by Adam Grabowski
::
:: Received October 22, 2015
:: Copyright (c) 2015-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, LATTICES, LATSTONE, XBOOLE_0, TARSKI, EQREL_1, PBOOLE,
ORDINAL4, XXREAL_2, STRUCT_0, ZFMISC_1, LATTICE5, FILTER_0, LATTICE4,
TOPS_1, REWRITE1, MOEBIUS2, NAT_1, FINSET_1, XCMPLX_0, MOEBIUS1, RELAT_1,
BINOP_1, REALSET1, LATTICEA, XXREAL_0, CARD_1, NUMBERS, NEWTON, ARYTM_3;
notations TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, ORDINAL1, NAT_1, FINSET_1,
ARYTM_3, BINOP_1, REALSET1, SUBSET_1, NAT_D, ENUMSET1, XCMPLX_0,
XXREAL_0, CARD_1, NUMBERS, NEWTON, INT_2, FUNCT_1, FUNCT_2, STRUCT_0,
LATTICES, LATTICE3, FILTER_0, FILTER_1, FILTER_2, LATTICE4, MOEBIUS1,
MOEBIUS2, LATTICEA;
constructors DOMAIN_1, XBOOLE_0, FILTER_1, NAT_1, ORDINAL1, INT_2, NEWTON,
ARYTM_3, NAT_D, SQUARE_1, ENUMSET1, ZFMISC_1, FILTER_0, FINSET_1,
FILTER_2, LATTICE4, MOEBIUS1, XREAL_0, XCMPLX_0, XXREAL_0, BINOP_1,
REALSET2, LATTICE3, PARTFUN1, MOEBIUS2, SUBSET_1, BOOLEALG, REALSET1,
LATTICEA;
registrations STRUCT_0, LATTICES, PARTFUN1, FUNCT_2, REALSET1, INT_1,
FILTER_1, LATTICE3, MOEBIUS1, MOEBIUS2, XCMPLX_0, CARD_1, INT_2, INT_3,
NEWTON, NAT_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, RELSET_1,
PBOOLE, LATTICE6;
requirements SUBSET, BOOLE, REAL, NUMERALS, ARITHM;
begin :: Preliminaries
:: The main aim of this article is to provide a formal counterpart
:: for the paper of Jouni J\"arvinen "Lattice theory for rough sets",
:: in Transactions of Rough Sets, VI, LNCS vol. 4374, pp. 400--498, 2007.
:: The corresponding items are marked by the acronym LTRS. We deal
:: with Section 4.3, page 423--426.
theorem :: LATSTONE:1
for L being distributive Lattice, S being Sublattice of L holds
S is distributive;
registration let L be distributive Lattice;
cluster -> distributive for Sublattice of L;
end;
registration let L1, L2 be bounded Lattice;
cluster [:L1,L2:] -> bounded;
end;
reserve L for Lattice;
reserve I,P for non empty ClosedSubset of L;
theorem :: LATSTONE:2
L is lower-bounded & Bottom L in I implies latt (L,I) is lower-bounded
& Bottom latt (L,I) = Bottom L;
theorem :: LATSTONE:3
L is upper-bounded & Top L in I implies latt (L,I) is upper-bounded
& Top latt (L,I) = Top L;
begin :: Pseudocomplements in Lattices
::$N Pseudocomplement
definition let L be non empty LattStr;
let a,b be Element of L;
pred a is_a_pseudocomplement_of b means
:: LATSTONE:def 1
a "/\" b = Bottom L &
for x being Element of L st b "/\" x = Bottom L holds x [= a;
end;
:: p. 122 6.1 Definition from Gratzer
definition let L be non empty LattStr;
attr L is pseudocomplemented means
:: LATSTONE:def 2
for x being Element of L
ex y being Element of L st y is_a_pseudocomplement_of x;
end;
:: LTRS: Example 43(a)
theorem :: LATSTONE:4
for L being Boolean Lattice holds L is pseudocomplemented;
registration
cluster Boolean -> pseudocomplemented for Lattice;
end;
registration
cluster Boolean pseudocomplemented bounded for Lattice;
end;
:: Pseudocomplements are unique
theorem :: LATSTONE:5
for L being pseudocomplemented lower-bounded Lattice,
a, b, x being Element of L st a is_a_pseudocomplement_of x &
b is_a_pseudocomplement_of x holds a = b;
:: The unique pseudocomplement
definition let L be non empty LattStr, x be Element of L;
assume L is pseudocomplemented lower-bounded Lattice;
func x* -> Element of L means
:: LATSTONE:def 3
it is_a_pseudocomplement_of x;
end;
theorem :: LATSTONE:6
for L being pseudocomplemented lower-bounded Lattice, x being Element of L
holds x* "/\" x = Bottom L;
reserve L for lower-bounded pseudocomplemented Lattice;
:: LTRS: Lemma 42(a)
theorem :: LATSTONE:7
for a being Element of L holds a [= a**;
:: LTRS: Lemma 42(b)
theorem :: LATSTONE:8
for a, b being Element of L holds a [= b implies b* [= a*;
:: LTRS: Lemma 42(c)
theorem :: LATSTONE:9
for a being Element of L holds a* = a***;
:: LTRS: Example 43(c)
theorem :: LATSTONE:10
for L being pseudocomplemented bounded Lattice holds (Bottom L)* = Top L;
:: LTRS: Example 43(c)
theorem :: LATSTONE:11
for L being pseudocomplemented bounded Lattice holds (Top L)* = Bottom L;
:: Pseudocomplements are precisely complements in complemented lattices.
:: A complement (if exists) is always a pseudocomplement.
:: LTRS: Example 43(a)
theorem :: LATSTONE:12
for L being Boolean Lattice, x being Element of L holds x` = x*;
:: Connection between pseudocomplements and the functor from LATTICEA
theorem :: LATSTONE:13
for L being pseudocomplemented bounded Lattice, x, y being Element of L st
y is_a_pseudocomplement_of x holds y in PseudoComplements x;
theorem :: LATSTONE:14
for L being pseudocomplemented bounded Lattice, x being Element of L holds
x* in PseudoComplements x;
begin :: Skeleton of a Pseudocomplemented Lattice
definition let L be lower-bounded pseudocomplemented Lattice;
func Skeleton L -> Subset of L equals
:: LATSTONE:def 4
the set of all a* where a is Element of L;
end;
theorem :: LATSTONE:15
for L being lower-bounded pseudocomplemented Lattice holds
Skeleton L = { a where a is Element of L : a** = a };
:: LTRS: Lemma 44(a), p. 424
theorem :: LATSTONE:16
for L being lower-bounded pseudocomplemented Lattice, x being Element of L
holds x in Skeleton L iff x** = x;
registration let L be bounded pseudocomplemented Lattice;
cluster Skeleton L -> non empty;
end;
theorem :: LATSTONE:17
for L being pseudocomplemented distributive lower-bounded Lattice holds
for a, b being Element of L st a in Skeleton L & b in Skeleton L holds
a "/\" b in Skeleton L;
begin :: Stone Identity
definition let L be non empty LattStr;
attr L is satisfying_Stone_identity means
:: LATSTONE:def 5
for x being Element of L holds x* "\/" (x**) = Top L;
end;
theorem :: LATSTONE:18
for L being Boolean Lattice holds L is satisfying_Stone_identity;
registration
cluster Boolean -> satisfying_Stone_identity for Lattice;
end;
registration
cluster satisfying_Stone_identity pseudocomplemented Boolean for Lattice;
end;
:: LTRS: Lemma 44(b), p. 424
theorem :: LATSTONE:19
for L being pseudocomplemented distributive bounded Lattice holds
L is satisfying_Stone_identity iff for a, b being Element of L holds
(a "/\" b)* = (a*) "\/" (b*);
::$N Stone algebra
definition
let L be Lattice;
attr L is Stone means
:: LATSTONE:def 6
L is pseudocomplemented distributive bounded satisfying_Stone_identity;
end;
registration
cluster Stone ->
pseudocomplemented distributive bounded satisfying_Stone_identity
for Lattice;
cluster pseudocomplemented distributive bounded satisfying_Stone_identity
-> Stone for Lattice;
end;
:: LTRS:
theorem :: LATSTONE:20
for L being pseudocomplemented distributive bounded Lattice holds
L is satisfying_Stone_identity iff for a, b being Element of L st
a in Skeleton L & b in Skeleton L holds a "\/" b in Skeleton L;
reserve L for Stone Lattice;
:: LTRS: Proposition 45
theorem :: LATSTONE:21
Top L in Skeleton L & Bottom L in Skeleton L;
definition let L be Stone Lattice, a be Element of L;
attr a is skeletal means
:: LATSTONE:def 7
a in Skeleton L;
end;
registration
let L be Stone Lattice;
cluster Top L -> skeletal;
cluster Bottom L -> skeletal;
end;
:: LTRS: Proposition 45
registration let L be Stone Lattice;
cluster Skeleton L -> join-closed meet-closed;
end;
definition let L be Stone Lattice;
redefine func Skeleton L -> ClosedSubset of L;
end;
:: Skeleton equipped with the lattice structure
definition let L be Stone Lattice;
func SkelLatt L -> Sublattice of L equals
:: LATSTONE:def 8
latt (L,Skeleton L);
end;
registration let L be Stone Lattice;
cluster SkelLatt L -> distributive;
end;
theorem :: LATSTONE:22
Bottom L = Bottom SkelLatt L & Top L = Top SkelLatt L;
:: LTRS: Proposition 45
registration let L be Stone Lattice;
cluster SkelLatt L -> Boolean;
end;
begin :: Dense Elements in Lattices
definition let L be lower-bounded Lattice;
func DenseElements L -> Subset of L equals
:: LATSTONE:def 9
{ a where a is Element of L : a* = Bottom L };
end;
theorem :: LATSTONE:23
Top L in DenseElements L;
registration let L be Stone Lattice;
cluster DenseElements L -> non empty;
end;
definition let L be Stone Lattice, a be Element of L;
attr a is dense means
:: LATSTONE:def 10
a in DenseElements L;
end;
registration let L be Stone Lattice;
cluster Top L -> dense;
end;
theorem :: LATSTONE:24
for L being Stone Lattice, x being Element of L st x in DenseElements L holds
x* = Bottom L;
registration let L be Stone Lattice;
cluster DenseElements L -> join-closed meet-closed;
end;
definition let L be Stone Lattice;
redefine func DenseElements L -> ClosedSubset of L;
end;
:: Set of dense elements equipped with the lattice structure
definition let L be Stone Lattice;
func DenseLatt L -> Sublattice of L equals
:: LATSTONE:def 11
latt (L, DenseElements L);
end;
registration let L be Stone Lattice;
cluster DenseLatt L -> distributive;
end;
:: Meet-decomposition of elements of a lattice in terms
:: of skeletal and dense elements
theorem :: LATSTONE:25
for L being Stone Lattice, a being Element of L holds
ex b, c being Element of L st a = b "/\" c & b in Skeleton L &
c in DenseElements L;
begin :: An Example: Lattice of Natural Divisors
theorem :: LATSTONE:26
for p being Prime holds NatDivisors p = {1, p};
theorem :: LATSTONE:27
for p being Prime holds NatDivisors (p * p) = {1, p, p*p};
registration let n be non zero Nat;
cluster Divisors_Lattice n -> finite;
end;
registration
cluster complete for Boolean Lattice;
end;
registration let p be Prime;
cluster Divisors_Lattice (p) -> Boolean;
end;
:: Hence it is pseudocomplemented, and Stone
registration let p be Prime;
cluster Divisors_Lattice (p * p) -> pseudocomplemented;
end;
theorem :: LATSTONE:28
for L being Lattice, p being Prime, x being Element of L st
L = Divisors_Lattice (p * p) & x = p holds x* = Bottom L;
:: The example of a lattice which is Stone but not Boolean
registration let p be Prime;
cluster Divisors_Lattice (p * p) -> satisfying_Stone_identity;
end;
registration let p be Prime;
cluster Divisors_Lattice (p * p) -> non Boolean Stone;
end;
registration
cluster Stone non Boolean for Lattice;
end;
:: Every squarefree number generates Stone lattice as it is Boolean
begin :: Products of Pseudocomplemented Lattices
reserve L1, L2 for Lattice;
reserve p1, q1 for Element of L1;
reserve p2, q2 for Element of L2;
theorem :: LATSTONE:29
L1 is 01_Lattice & L2 is 01_Lattice implies
(p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2 iff
[p1,p2] is_a_pseudocomplement_of [q1,q2]);
theorem :: LATSTONE:30
L1 is 01_Lattice & L2 is 01_Lattice implies (L1 is pseudocomplemented &
L2 is pseudocomplemented iff [:L1,L2:] is pseudocomplemented);
registration let L1, L2 be pseudocomplemented 01_Lattice;
cluster [:L1,L2:] -> pseudocomplemented;
end;
theorem :: LATSTONE:31
L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice
implies [p1,p2]* = [p1*,p2*];
reserve L1, L2 for non empty Lattice;
theorem :: LATSTONE:32
L1 is satisfying_Stone_identity pseudocomplemented 01_Lattice &
L2 is satisfying_Stone_identity pseudocomplemented 01_Lattice implies
[:L1,L2:] is satisfying_Stone_identity;
theorem :: LATSTONE:33
L1 is Stone & L2 is Stone implies [:L1,L2:] is Stone;
registration let L1, L2 be Stone Lattice;
cluster [:L1,L2:] -> Stone;
end;
begin :: Special Construction: B squared
reserve B for Boolean Lattice;
:: LTRS: Lemma 46 - definition
definition let B be Boolean Lattice;
func B squared -> Subset of [:B,B:] equals
:: LATSTONE:def 12
{ [a,b] where a, b is Element of B : a [= b };
end;
registration let B be Boolean Lattice;
cluster B squared -> non empty;
end;
registration let B be Boolean Lattice;
cluster B squared -> join-closed meet-closed;
end;
definition let B be Boolean Lattice;
redefine func B squared -> non empty ClosedSubset of [:B,B:];
end;
definition let B be Boolean Lattice;
func B squared-latt -> Lattice equals
:: LATSTONE:def 13
latt ([:B,B:], B squared);
end;
theorem :: LATSTONE:34
the carrier of (B squared-latt) = B squared;
theorem :: LATSTONE:35
[Bottom B, Bottom B] in the carrier of (B squared-latt);
theorem :: LATSTONE:36
[Top B, Top B] in the carrier of (B squared-latt);
registration let B be Boolean Lattice;
cluster B squared-latt -> lower-bounded;
cluster B squared-latt -> upper-bounded;
end;
theorem :: LATSTONE:37
Bottom (B squared-latt) = [Bottom B, Bottom B];
theorem :: LATSTONE:38
Top (B squared-latt) = [Top B, Top B];
registration let B be Boolean Lattice;
cluster B squared-latt -> pseudocomplemented;
end;
theorem :: LATSTONE:39
for L being Lattice, x1,x2 being Element of B, x being Element of L st
L = B squared-latt & x = [x1,x2] holds x* = [x2`,x2`];
registration let B be Boolean Lattice;
cluster B squared-latt -> satisfying_Stone_identity;
end;
:: LTRS: Lemma 46, p. 425
registration let B be Boolean Lattice;
cluster B squared-latt -> Stone;
end;
:: Skeleton and dense elements in the lattice B squared
theorem :: LATSTONE:40
Skeleton (B squared-latt) = the set of all [a,a] where a is Element of B;
theorem :: LATSTONE:41
DenseElements (B squared-latt) = the set of all [a,Top B]
where a is Element of B;