:: by Adam Grabowski

::

:: Received October 22, 2015

:: Copyright (c) 2015-2019 Association of Mizar Users

registration

let L be distributive Lattice;

coherence

for b_{1} being Sublattice of L holds b_{1} is distributive
by ThA;

end;
coherence

for b

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 )

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 )

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;

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

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 ;

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

for x being Element of L ex y being Element of L st y is_a_pseudocomplement_of x;

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

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)

registration
end;

registration

ex b_{1} being Lattice st

( b_{1} is Boolean & b_{1} is pseudocomplemented & b_{1} is bounded )
end;

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

( b

proof 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

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 ;

existence

ex b_{1} being Element of L st b_{1} is_a_pseudocomplement_of x
by def2, A1;

uniqueness

for b_{1}, b_{2} being Element of L st b_{1} is_a_pseudocomplement_of x & b_{2} is_a_pseudocomplement_of x holds

b_{1} = b_{2}
by A1, Th2;

end;
let x be Element of L;

assume A1: L is lower-bounded pseudocomplemented Lattice ;

existence

ex b

uniqueness

for b

b

:: 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_{3} being Element of L holds

( b_{3} = x * iff b_{3} is_a_pseudocomplement_of x );

for L being non empty LattStr

for x being Element of L st L is lower-bounded pseudocomplemented Lattice holds

for b

( b

theorem ThD: :: LATSTONE:6

for L being lower-bounded pseudocomplemented Lattice

for x being Element of L holds (x *) "/\" x = Bottom L

for x being Element of L holds (x *) "/\" x = Bottom L

proof end;

:: LTRS: Lemma 42(a)

:: 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 *

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 *) *) *

for a being Element of L holds a * = ((a *) *) *

proof end;

:: LTRS: Example 43(c)

:: LTRS: Example 43(c)

:: Pseudocomplements are precisely complements in complemented lattices.

:: A complement (if exists) is always a pseudocomplement.

:: LTRS: Example 43(a)

:: A complement (if exists) is always a pseudocomplement.

:: LTRS: Example 43(a)

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

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

for x being Element of L holds x * in PseudoComplements x

proof end;

definition

let L be lower-bounded pseudocomplemented Lattice;

coherence

{ (a *) where a is Element of L : verum } is Subset of L

end;
coherence

{ (a *) where a is Element of L : verum } is Subset of L

proof 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 } ;

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 )

for x being Element of L holds

( x in Skeleton L iff (x *) * = x )

proof end;

registration
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

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 ;

end;
attr L is satisfying_Stone_identity means :SatStone: :: LATSTONE:def 5

for x being Element of L holds (x *) "\/" ((x *) *) = Top L;

for x being Element of L holds (x *) "\/" ((x *) *) = Top L;

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

for L being non empty LattStr holds

( L is satisfying_Stone_identity iff for x being Element of L holds (x *) "\/" ((x *) *) = Top L );

registration

coherence

for b_{1} being Lattice st b_{1} is Boolean holds

b_{1} is satisfying_Stone_identity
by Th4;

end;
for b

b

registration

ex b_{1} being Lattice st

( b_{1} is satisfying_Stone_identity & b_{1} is pseudocomplemented & b_{1} is Boolean )
end;

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

( b

proof 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 *) )

( L is satisfying_Stone_identity iff for a, b being Element of L holds (a "/\" b) * = (a *) "\/" (b *) )

proof end;

definition

let L be Lattice;

end;
attr L is Stone means :: LATSTONE:def 6

( L is pseudocomplemented & L is distributive & L is bounded & L is satisfying_Stone_identity );

( L is pseudocomplemented & L is distributive & L is bounded & L is satisfying_Stone_identity );

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

for L being Lattice holds

( L is Stone iff ( L is pseudocomplemented & L is distributive & L is bounded & L is satisfying_Stone_identity ) );

registration

for b_{1} being Lattice st b_{1} is Stone holds

( b_{1} is pseudocomplemented & b_{1} is distributive & b_{1} is bounded & b_{1} is satisfying_Stone_identity )
;

for b_{1} being Lattice st b_{1} is pseudocomplemented & b_{1} is distributive & b_{1} is bounded & b_{1} is satisfying_Stone_identity holds

b_{1} is Stone
;

end;

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

coherence for b

( b

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

coherence for b

b

:: 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 )

( 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

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

for L being Stone Lattice

for a being Element of L holds

( a is skeletal iff a in Skeleton L );

registration
end;

:: LTRS: Proposition 45

registration

let L be Stone Lattice;

coherence

( Skeleton L is join-closed & Skeleton L is meet-closed )

end;
coherence

( Skeleton L is join-closed & Skeleton L is meet-closed )

proof end;

definition

let L be Stone Lattice;

:: original: Skeleton

redefine func Skeleton L -> ClosedSubset of L;

coherence

Skeleton L is ClosedSubset of L ;

end;
:: original: Skeleton

redefine func Skeleton L -> ClosedSubset of L;

coherence

Skeleton L is ClosedSubset of L ;

:: Skeleton equipped with the lattice structure

:: deftheorem defines SkelLatt LATSTONE:def 8 :

for L being Stone Lattice holds SkelLatt L = latt (L,(Skeleton L));

for L being Stone Lattice holds SkelLatt L = latt (L,(Skeleton L));

registration
end;

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

proof end;

:: LTRS: Proposition 45

registration
end;

definition

let L be lower-bounded Lattice;

{ a where a is Element of L : a * = Bottom L } is Subset of L

end;
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 } ;

{ a where a is Element of L : a * = Bottom L } is Subset of L

proof 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 } ;

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

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

for L being Stone Lattice

for a being Element of L holds

( a is dense iff a in DenseElements L );

registration
end;

registration

let L be Stone Lattice;

coherence

( DenseElements L is join-closed & DenseElements L is meet-closed )

end;
coherence

( DenseElements L is join-closed & DenseElements L is meet-closed )

proof end;

definition

let L be Stone Lattice;

:: original: DenseElements

redefine func DenseElements L -> ClosedSubset of L;

coherence

DenseElements L is ClosedSubset of L ;

end;
:: original: DenseElements

redefine func DenseElements L -> ClosedSubset of L;

coherence

DenseElements L is ClosedSubset of L ;

:: Set of dense elements equipped with the lattice structure

:: deftheorem defines DenseLatt LATSTONE:def 11 :

for L being Stone Lattice holds DenseLatt L = latt (L,(DenseElements L));

for L being Stone Lattice holds DenseLatt L = latt (L,(DenseElements L));

:: Meet-decomposition of elements of a lattice in terms

:: of skeletal and dense elements

:: 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 )

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;

registration

ex b_{1} being Boolean Lattice st b_{1} is complete
end;

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

proof end;

:: Hence it is pseudocomplemented, and Stone

registration
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

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
end;

registration

let p be Prime;

coherence

( not Divisors_Lattice (p * p) is Boolean & Divisors_Lattice (p * p) is Stone )

end;
coherence

( not Divisors_Lattice (p * p) is Boolean & Divisors_Lattice (p * p) is Stone )

proof end;

registration

ex b_{1} being Lattice st

( b_{1} is Stone & not b_{1} is Boolean )
end;

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

( b

proof 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] )

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 )

( ( L1 is pseudocomplemented & L2 is pseudocomplemented ) iff [:L1,L2:] is pseudocomplemented )

proof end;

registration

let L1, L2 be pseudocomplemented 01_Lattice;

coherence

[:L1,L2:] is pseudocomplemented by PsComplProduct;

end;
coherence

[:L1,L2:] is pseudocomplemented by PsComplProduct;

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 *)]

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

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

[:L1,L2:] is Stone by ProductIsSStone, FILTER_1:38;

registration
end;

:: LTRS: Lemma 46 - definition

definition

let B be Boolean Lattice;

{ [a,b] where a, b is Element of B : a [= b } is Subset of [:B,B:]

end;
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 } ;

{ [a,b] where a, b is Element of B : a [= b } is Subset of [:B,B:]

proof 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 } ;

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;

coherence

( B squared is join-closed & B squared is meet-closed )

end;
coherence

( B squared is join-closed & B squared is meet-closed )

proof 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;
:: original: squared

redefine func B squared -> non empty ClosedSubset of [:B,B:];

coherence

B squared is non empty ClosedSubset of [:B,B:] ;

:: deftheorem defines squared-latt LATSTONE:def 13 :

for B being Boolean Lattice holds B squared-latt = latt ([:B,B:],(B squared));

for B being Boolean Lattice holds B squared-latt = latt ([:B,B:],(B squared));

registration

let B be Boolean Lattice;

coherence

B squared-latt is lower-bounded

B squared-latt is upper-bounded

end;
coherence

B squared-latt is lower-bounded

proof end;

coherence B squared-latt is upper-bounded

proof end;

registration
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 `)]

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
end;

:: LTRS: Lemma 46, p. 425

registration
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;

:: 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.