:: 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 b₁ being Sublattice of L holds b₁ 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;

:: 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 b₁ being Lattice st b₁ is Boolean holds
b₁ 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 b₁ being Lattice st
( b₁ is Boolean & b₁ is pseudocomplemented & b₁ 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 b₁ being Element of L st b₁ is_a_pseudocomplement_of x by def2, A1;
uniqueness
for b₁, b₂ being Element of L st b₁ is_a_pseudocomplement_of x & b₂ is_a_pseudocomplement_of x holds
b₁ = b₂ 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 b₃ being Element of L holds
( b₃ = x * iff b₃ 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 b₁ being Lattice st b₁ is Boolean holds
b₁ 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 b₁ being Lattice st
( b₁ is satisfying_Stone_identity & b₁ is pseudocomplemented & b₁ 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;

:: 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 b₁ being Lattice st b₁ is Stone holds
( b₁ is pseudocomplemented & b₁ is distributive & b₁ is bounded & b₁ is satisfying_Stone_identity ) ;

cluster non empty Lattice-like distributive bounded pseudocomplemented satisfying_Stone_identity -> Stone for LattStr ;

coherence
for b₁ being Lattice st b₁ is pseudocomplemented & b₁ is distributive & b₁ is bounded & b₁ is satisfying_Stone_identity holds
b₁ 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 b₁ being Boolean Lattice st b₁ 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 b₁ being Lattice st
( b₁ is Stone & not b₁ 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;