:: Stone Lattices
:: by Adam Grabowski
::
:: Received October 22, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


:: 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 ThA: :: LATSTONE:1
for L being distributive Lattice
for S being Sublattice of L holds S is distributive
proof end;

registration
let L be distributive Lattice;
cluster -> distributive for Sublattice of L;
coherence
for b1 being Sublattice of L holds b1 is distributive
by ThA;
end;

registration
let L1, L2 be bounded Lattice;
cluster [:L1,L2:] -> bounded ;
coherence
[:L1,L2:] is bounded
by FILTER_1:41;
end;

theorem ThB: :: LATSTONE:2
for L being Lattice
for I being non empty ClosedSubset of L st L is lower-bounded & Bottom L in I holds
( latt (L,I) is lower-bounded & Bottom (latt (L,I)) = Bottom L )
proof end;

theorem ThC: :: LATSTONE:3
for L being Lattice
for I being non empty ClosedSubset of L st L is upper-bounded & Top L in I holds
( latt (L,I) is upper-bounded & Top (latt (L,I)) = Top L )
proof end;

:: WP: 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;

:: deftheorem defines is_a_pseudocomplement_of LATSTONE:def 1 :
for L being non empty LattStr
for a, b being Element of L holds
( a is_a_pseudocomplement_of b iff ( a "/\" b = Bottom L & ( for x being Element of L st b "/\" x = Bottom L holds
x [= a ) ) );

:: p. 122 6.1 Definition from Gratzer
definition
let L be non empty LattStr ;
:: p. 122 6.1 Definition from Gratzer
attr L is pseudocomplemented means :def2: :: LATSTONE:def 2
for x being Element of L ex y being Element of L st y is_a_pseudocomplement_of x;
end;

:: deftheorem def2 defines pseudocomplemented LATSTONE:def 2 :
for L being non empty LattStr holds
( L is pseudocomplemented iff for x being Element of L ex y being Element of L st y is_a_pseudocomplement_of x );

:: LTRS: Example 43(a)
theorem Th1: :: LATSTONE:4
for L being Boolean Lattice holds L is pseudocomplemented
proof end;

registration
cluster non empty Lattice-like Boolean -> pseudocomplemented for LattStr ;
coherence
for b1 being Lattice st b1 is Boolean holds
b1 is pseudocomplemented
by Th1;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded Boolean pseudocomplemented for LattStr ;
existence
ex b1 being Lattice st
( b1 is Boolean & b1 is pseudocomplemented & b1 is bounded )
proof end;
end;

:: Pseudocomplements are unique
theorem Th2: :: LATSTONE:5
for L being lower-bounded pseudocomplemented Lattice
for a, b, x being Element of L st a is_a_pseudocomplement_of x & b is_a_pseudocomplement_of x holds
a = b
proof end;

:: The unique pseudocomplement
definition
let L be non empty LattStr ;
let x be Element of L;
assume A1: L is lower-bounded pseudocomplemented Lattice ;
func x * -> Element of L means :def3: :: LATSTONE:def 3
it is_a_pseudocomplement_of x;
existence
ex b1 being Element of L st b1 is_a_pseudocomplement_of x
by def2, A1;
uniqueness
for b1, b2 being Element of L st b1 is_a_pseudocomplement_of x & b2 is_a_pseudocomplement_of x holds
b1 = b2
by A1, Th2;
end;

:: deftheorem def3 defines * LATSTONE:def 3 :
for L being non empty LattStr
for x being Element of L st L is lower-bounded pseudocomplemented Lattice holds
for b3 being Element of L holds
( b3 = x * iff b3 is_a_pseudocomplement_of x );

theorem ThD: :: LATSTONE:6
for L being lower-bounded pseudocomplemented Lattice
for x being Element of L holds (x *) "/\" x = Bottom L
proof end;

:: LTRS: Lemma 42(a)
theorem Th5: :: LATSTONE:7
for L being lower-bounded pseudocomplemented Lattice
for a being Element of L holds a [= (a *) *
proof end;

:: LTRS: Lemma 42(b)
theorem Th6: :: LATSTONE:8
for L being lower-bounded pseudocomplemented Lattice
for a, b being Element of L st a [= b holds
b * [= a *
proof end;

:: LTRS: Lemma 42(c)
theorem Th7: :: LATSTONE:9
for L being lower-bounded pseudocomplemented Lattice
for a being Element of L holds a * = ((a *) *) *
proof end;

:: LTRS: Example 43(c)
theorem Th11: :: LATSTONE:10
for L being bounded pseudocomplemented Lattice holds (Bottom L) * = Top L
proof end;

:: LTRS: Example 43(c)
theorem Th11a: :: LATSTONE:11
for L being bounded pseudocomplemented Lattice holds (Top L) * = Bottom L
proof end;

:: Pseudocomplements are precisely complements in complemented lattices.
:: A complement (if exists) is always a pseudocomplement.
:: LTRS: Example 43(a)
theorem ThE: :: LATSTONE:12
for L being Boolean Lattice
for x being Element of L holds x ` = x *
proof end;

:: Connection between pseudocomplements and the functor from LATTICEA
theorem ThF: :: LATSTONE:13
for L being bounded pseudocomplemented Lattice
for x, y being Element of L st y is_a_pseudocomplement_of x holds
y in PseudoComplements x
proof end;

theorem :: LATSTONE:14
for L being bounded pseudocomplemented Lattice
for x being Element of L holds x * in PseudoComplements x
proof end;

definition
let L be lower-bounded pseudocomplemented Lattice;
func Skeleton L -> Subset of L equals :: LATSTONE:def 4
{ (a *) where a is Element of L : verum } ;
coherence
{ (a *) where a is Element of L : verum } is Subset of L
proof end;
end;

:: deftheorem defines Skeleton LATSTONE:def 4 :
for L being lower-bounded pseudocomplemented Lattice holds Skeleton L = { (a *) where a is Element of L : verum } ;

theorem :: LATSTONE:15
for L being lower-bounded pseudocomplemented Lattice holds Skeleton L = { a where a is Element of L : (a *) * = a }
proof end;

:: LTRS: Lemma 44(a), p. 424
theorem Th13: :: LATSTONE:16
for L being lower-bounded pseudocomplemented Lattice
for x being Element of L holds
( x in Skeleton L iff (x *) * = x )
proof end;

registration
let L be bounded pseudocomplemented Lattice;
cluster Skeleton L -> non empty ;
coherence
not Skeleton L is empty
proof end;
end;

theorem :: LATSTONE:17
for L being distributive lower-bounded pseudocomplemented Lattice
for a, b being Element of L st a in Skeleton L & b in Skeleton L holds
a "/\" b in Skeleton L
proof end;

definition
let L be non empty LattStr ;
attr L is satisfying_Stone_identity means :SatStone: :: LATSTONE:def 5
for x being Element of L holds (x *) "\/" ((x *) *) = Top L;
end;

:: deftheorem SatStone defines satisfying_Stone_identity LATSTONE:def 5 :
for L being non empty LattStr holds
( L is satisfying_Stone_identity iff for x being Element of L holds (x *) "\/" ((x *) *) = Top L );

theorem Th4: :: LATSTONE:18
for L being Boolean Lattice holds L is satisfying_Stone_identity
proof end;

registration
cluster non empty Lattice-like Boolean -> satisfying_Stone_identity for LattStr ;
coherence
for b1 being Lattice st b1 is Boolean holds
b1 is satisfying_Stone_identity
by Th4;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean pseudocomplemented satisfying_Stone_identity for LattStr ;
existence
ex b1 being Lattice st
( b1 is satisfying_Stone_identity & b1 is pseudocomplemented & b1 is Boolean )
proof end;
end;

:: LTRS: Lemma 44(b), p. 424
theorem Th12: :: LATSTONE:19
for L being distributive bounded pseudocomplemented Lattice holds
( L is satisfying_Stone_identity iff for a, b being Element of L holds (a "/\" b) * = (a *) "\/" (b *) )
proof end;

:: WP: Stone algebra
definition
let L be Lattice;
attr L is Stone means :: LATSTONE:def 6
( L is pseudocomplemented & L is distributive & L is bounded & L is satisfying_Stone_identity );
end;

:: deftheorem defines Stone LATSTONE:def 6 :
for L being Lattice holds
( L is Stone iff ( L is pseudocomplemented & L is distributive & L is bounded & L is satisfying_Stone_identity ) );

registration
cluster non empty Lattice-like Stone -> distributive bounded pseudocomplemented satisfying_Stone_identity for LattStr ;
coherence
for b1 being Lattice st b1 is Stone holds
( b1 is pseudocomplemented & b1 is distributive & b1 is bounded & b1 is satisfying_Stone_identity )
;
cluster non empty Lattice-like distributive bounded pseudocomplemented satisfying_Stone_identity -> Stone for LattStr ;
coherence
for b1 being Lattice st b1 is pseudocomplemented & b1 is distributive & b1 is bounded & b1 is satisfying_Stone_identity holds
b1 is Stone
;
end;

:: LTRS:
theorem :: LATSTONE:20
for L being distributive bounded pseudocomplemented 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 )
proof end;

:: LTRS: Proposition 45
theorem Lm1: :: LATSTONE:21
for L being Stone Lattice holds
( Top L in Skeleton L & Bottom L in Skeleton L )
proof end;

definition
let L be Stone Lattice;
let a be Element of L;
attr a is skeletal means :: LATSTONE:def 7
a in Skeleton L;
end;

:: deftheorem defines skeletal LATSTONE:def 7 :
for L being Stone Lattice
for a being Element of L holds
( a is skeletal iff a in Skeleton L );

registration
let L be Stone Lattice;
cluster Top L -> skeletal ;
coherence
Top L is skeletal
by Lm1;
cluster Bottom L -> skeletal ;
coherence
Bottom L is skeletal
by Lm1;
end;

:: LTRS: Proposition 45
registration
let L be Stone Lattice;
cluster Skeleton L -> meet-closed join-closed ;
coherence
( Skeleton L is join-closed & Skeleton L is meet-closed )
proof end;
end;

definition
let L be Stone Lattice;
:: original: Skeleton
redefine func Skeleton L -> ClosedSubset of L;
coherence
Skeleton L is 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));
coherence
latt (L,(Skeleton L)) is Sublattice of L
;
end;

:: deftheorem defines SkelLatt LATSTONE:def 8 :
for L being Stone Lattice holds SkelLatt L = latt (L,(Skeleton L));

registration
let L be Stone Lattice;
cluster SkelLatt L -> distributive ;
coherence
SkelLatt L is distributive
;
end;

theorem :: LATSTONE:22
for L being Stone Lattice holds
( Bottom L = Bottom (SkelLatt L) & Top L = Top (SkelLatt L) )
proof end;

LattIsComplemented: for L being Stone Lattice holds latt (L,(Skeleton L)) is complemented
proof end;

:: LTRS: Proposition 45
registration
let L be Stone Lattice;
cluster SkelLatt L -> Boolean ;
coherence
SkelLatt L is Boolean
proof end;
end;

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 } ;
coherence
{ a where a is Element of L : a * = Bottom L } is Subset of L
proof end;
end;

:: deftheorem defines DenseElements LATSTONE:def 9 :
for L being lower-bounded Lattice holds DenseElements L = { a where a is Element of L : a * = Bottom L } ;

theorem TopIsDense: :: LATSTONE:23
for L being Stone Lattice holds Top L in DenseElements L
proof end;

registration
let L be Stone Lattice;
cluster DenseElements L -> non empty ;
coherence
not DenseElements L is empty
by TopIsDense;
end;

definition
let L be Stone Lattice;
let a be Element of L;
attr a is dense means :: LATSTONE:def 10
a in DenseElements L;
end;

:: deftheorem defines dense LATSTONE:def 10 :
for L being Stone Lattice
for a being Element of L holds
( a is dense iff a in DenseElements L );

registration
let L be Stone Lattice;
cluster Top L -> dense ;
coherence
Top L is dense
by TopIsDense;
end;

theorem DenseIsBot: :: LATSTONE:24
for L being Stone Lattice
for x being Element of L st x in DenseElements L holds
x * = Bottom L
proof end;

registration
let L be Stone Lattice;
cluster DenseElements L -> meet-closed join-closed ;
coherence
( DenseElements L is join-closed & DenseElements L is meet-closed )
proof end;
end;

definition
let L be Stone Lattice;
:: original: DenseElements
redefine func DenseElements L -> ClosedSubset of L;
coherence
DenseElements L is 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));
coherence
latt (L,(DenseElements L)) is Sublattice of L
;
end;

:: deftheorem defines DenseLatt LATSTONE:def 11 :
for L being Stone Lattice holds DenseLatt L = latt (L,(DenseElements L));

registration
let L be Stone Lattice;
cluster DenseLatt L -> distributive ;
coherence
DenseLatt L is distributive
;
end;

:: Meet-decomposition of elements of a lattice in terms
:: of skeletal and dense elements
theorem :: LATSTONE:25
for L being Stone Lattice
for a being Element of L ex b, c being Element of L st
( a = b "/\" c & b in Skeleton L & c in DenseElements L )
proof end;

theorem :: LATSTONE:26
for p being Prime holds NatDivisors p = {1,p}
proof end;

theorem DivisorsSquare: :: LATSTONE:27
for p being Prime holds NatDivisors (p * p) = {1,p,(p * p)}
proof end;

registration
let n be non zero Nat;
cluster Divisors_Lattice n -> finite ;
coherence
Divisors_Lattice n is finite
proof end;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean complete pseudocomplemented satisfying_Stone_identity Stone for LattStr ;
existence
ex b1 being Boolean Lattice st b1 is complete
proof end;
end;

registration
let p be Prime;
cluster Divisors_Lattice p -> Boolean ;
coherence
Divisors_Lattice p is Boolean
proof end;
end;

:: Hence it is pseudocomplemented, and Stone
registration
let p be Prime;
cluster Divisors_Lattice (p * p) -> pseudocomplemented ;
coherence
Divisors_Lattice (p * p) is pseudocomplemented
proof end;
end;

theorem PsCompl: :: LATSTONE:28
for L being Lattice
for p being Prime
for x being Element of L st L = Divisors_Lattice (p * p) & x = p holds
x * = Bottom L
proof end;

:: The example of a lattice which is Stone but not Boolean
registration
let p be Prime;
cluster Divisors_Lattice (p * p) -> satisfying_Stone_identity ;
coherence
Divisors_Lattice (p * p) is satisfying_Stone_identity
proof end;
end;

registration
let p be Prime;
cluster Divisors_Lattice (p * p) -> non Boolean Stone ;
coherence
( not Divisors_Lattice (p * p) is Boolean & Divisors_Lattice (p * p) is Stone )
proof end;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like non Boolean Stone for LattStr ;
existence
ex b1 being Lattice st
( b1 is Stone & not b1 is Boolean )
proof end;
end;

theorem ProductPsCompl: :: LATSTONE:29
for L1, L2 being Lattice
for p1, q1 being Element of L1
for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( p1 is_a_pseudocomplement_of q1 & p2 is_a_pseudocomplement_of q2 ) iff [p1,p2] is_a_pseudocomplement_of [q1,q2] )
proof end;

theorem PsComplProduct: :: LATSTONE:30
for L1, L2 being Lattice st L1 is 01_Lattice & L2 is 01_Lattice holds
( ( L1 is pseudocomplemented & L2 is pseudocomplemented ) iff [:L1,L2:] is pseudocomplemented )
proof end;

registration
let L1, L2 be pseudocomplemented 01_Lattice;
cluster [:L1,L2:] -> pseudocomplemented ;
coherence
[:L1,L2:] is pseudocomplemented
by PsComplProduct;
end;

theorem ProductPCompl: :: LATSTONE:31
for L1, L2 being Lattice
for p1 being Element of L1
for p2 being Element of L2 st L1 is pseudocomplemented 01_Lattice & L2 is pseudocomplemented 01_Lattice holds
[p1,p2] * = [(p1 *),(p2 *)]
proof end;

theorem ProductIsSStone: :: LATSTONE:32
for L1, L2 being Lattice st L1 is pseudocomplemented satisfying_Stone_identity 01_Lattice & L2 is pseudocomplemented satisfying_Stone_identity 01_Lattice holds
[:L1,L2:] is satisfying_Stone_identity
proof end;

theorem :: LATSTONE:33
for L1, L2 being Lattice st L1 is Stone & L2 is Stone holds
[:L1,L2:] is Stone by ProductIsSStone, FILTER_1:38;

registration
let L1, L2 be Stone Lattice;
cluster [:L1,L2:] -> Stone ;
coherence
[:L1,L2:] is Stone
by ProductIsSStone, FILTER_1:38;
end;

:: 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 } ;
coherence
{ [a,b] where a, b is Element of B : a [= b } is Subset of [:B,B:]
proof end;
end;

:: deftheorem defines squared LATSTONE:def 12 :
for B being Boolean Lattice holds B squared = { [a,b] where a, b is Element of B : a [= b } ;

registration
let B be Boolean Lattice;
cluster B squared -> non empty ;
coherence
not B squared is empty
proof end;
end;

registration
let B be Boolean Lattice;
cluster B squared -> meet-closed join-closed ;
coherence
( B squared is join-closed & B squared is meet-closed )
proof end;
end;

definition
let B be Boolean Lattice;
:: original: squared
redefine func B squared -> non empty ClosedSubset of [:B,B:];
coherence
B squared is 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));
coherence
latt ([:B,B:],(B squared)) is Lattice
;
end;

:: deftheorem defines squared-latt LATSTONE:def 13 :
for B being Boolean Lattice holds B squared-latt = latt ([:B,B:],(B squared));

theorem SquaredCarrier: :: LATSTONE:34
for B being Boolean Lattice holds the carrier of (B squared-latt) = B squared
proof end;

theorem :: LATSTONE:35
for B being Boolean Lattice holds [(Bottom B),(Bottom B)] in the carrier of (B squared-latt)
proof end;

theorem :: LATSTONE:36
for B being Boolean Lattice holds [(Top B),(Top B)] in the carrier of (B squared-latt)
proof end;

registration
let B be Boolean Lattice;
cluster B squared-latt -> lower-bounded ;
coherence
B squared-latt is lower-bounded
proof end;
cluster B squared-latt -> upper-bounded ;
coherence
B squared-latt is upper-bounded
proof end;
end;

theorem SquaredBottom: :: LATSTONE:37
for B being Boolean Lattice holds Bottom (B squared-latt) = [(Bottom B),(Bottom B)]
proof end;

theorem SquaredTop: :: LATSTONE:38
for B being Boolean Lattice holds Top (B squared-latt) = [(Top B),(Top B)]
proof end;

registration
let B be Boolean Lattice;
cluster B squared-latt -> pseudocomplemented ;
coherence
B squared-latt is pseudocomplemented
proof end;
end;

theorem PseudoInSquared: :: LATSTONE:39
for B being Boolean Lattice
for L being Lattice
for x1, x2 being Element of B
for x being Element of L st L = B squared-latt & x = [x1,x2] holds
x * = [(x2 `),(x2 `)]
proof end;

registration
let B be Boolean Lattice;
cluster B squared-latt -> satisfying_Stone_identity ;
coherence
B squared-latt is satisfying_Stone_identity
proof end;
end;

:: LTRS: Lemma 46, p. 425
registration
let B be Boolean Lattice;
cluster B squared-latt -> Stone ;
coherence
B squared-latt is Stone
;
end;

:: Skeleton and dense elements in the lattice B squared
theorem :: LATSTONE:40
for B being Boolean Lattice holds Skeleton (B squared-latt) = { [a,a] where a is Element of B : verum }
proof end;

theorem :: LATSTONE:41
for B being Boolean Lattice holds DenseElements (B squared-latt) = { [a,(Top B)] where a is Element of B : verum }
proof end;