Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Boolean Properties of Lattices

by
Agnieszka Julia Marasik

MML identifier: BOOLEALG
[ Mizar article, MML identifier index ]

```environ

vocabulary LATTICES, BOOLE, SUBSET_1;
notation STRUCT_0, LATTICES;
constructors LATTICES, XBOOLE_0;
clusters LATTICES, ZFMISC_1, XBOOLE_0;

begin :: General Lattices

reserve L for Lattice;
reserve X,Y,Z,V for Element of L;

definition let L,X,Y;
func X \ Y -> Element of L equals
:: BOOLEALG:def 1
X "/\" Y`;
end;

definition let L,X,Y;
func X \+\ Y -> Element of L equals
:: BOOLEALG:def 2
(X \ Y) "\/" (Y \ X);
end;

definition let L,X,Y;
redefine pred X = Y means
:: BOOLEALG:def 3
X [= Y & Y [= X;
end;

definition let L,X,Y;
pred X meets Y means
:: BOOLEALG:def 4
X "/\" Y <> Bottom L;
antonym X misses Y;
end;

canceled 2;

theorem :: BOOLEALG:3
X "\/" Y [= Z implies X [= Z & Y [= Z;

theorem :: BOOLEALG:4
X "/\" Y [= X "\/" Z;

canceled;

theorem :: BOOLEALG:6
X [= Z implies X \ Y [= Z;

theorem :: BOOLEALG:7
X [= Y implies X \ Z [= Y \ Z;

theorem :: BOOLEALG:8
X \ Y [= X;

theorem :: BOOLEALG:9
X \ Y [= X \+\ Y;

theorem :: BOOLEALG:10
X \ Y [= Z & Y \ X [= Z implies X \+\ Y [= Z;

theorem :: BOOLEALG:11
X = Y "\/" Z iff Y [= X & Z [= X & for V st Y [= V & Z [= V
holds X [= V;

theorem :: BOOLEALG:12
X = Y "/\" Z iff X [= Y & X [= Z & for V st V [= Y & V [= Z
holds V [= X;

canceled;

theorem :: BOOLEALG:14
X "/\" (Y \ Z) = (X "/\" Y) \ Z;

theorem :: BOOLEALG:15
X meets Y implies Y meets X;

theorem :: BOOLEALG:16
X meets X iff X <> Bottom L;

theorem :: BOOLEALG:17
X \+\ Y = Y \+\ X;

definition let L, X, Y;
redefine pred X meets Y;
symmetry;
redefine func X \+\ Y;
commutativity;
end;

begin :: Modular Lattices

reserve L for M_Lattice;
reserve X,Y for Element of L;

canceled 3;

theorem :: BOOLEALG:21
X misses Y implies Y misses X;

begin   ::Distributive Lattices

reserve L for D_Lattice;
reserve X,Y,Z for Element of L;

theorem :: BOOLEALG:22
(X "/\" Y) "\/" (X "/\" Z) = X implies X [= Y "\/" Z;

canceled;

theorem :: BOOLEALG:24
(X "\/" Y) \ Z = (X \ Z) "\/" (Y \ Z);

begin   ::Distributive bounded Lattices

reserve L for 0_Lattice;
reserve X,Y,Z for Element of L;

theorem :: BOOLEALG:25
X [= Bottom L implies X = Bottom L;

theorem :: BOOLEALG:26
X [= Y & X [= Z & Y "/\" Z = Bottom L implies X = Bottom L;

theorem :: BOOLEALG:27
X "\/" Y = Bottom L iff X = Bottom L & Y = Bottom L;

theorem :: BOOLEALG:28
X [= Y & Y "/\" Z = Bottom L implies X "/\" Z = Bottom L;

theorem :: BOOLEALG:29
Bottom L \ X = Bottom L;

theorem :: BOOLEALG:30
X meets Y & Y [= Z implies X meets Z;

theorem :: BOOLEALG:31
X meets Y "/\" Z implies X meets Y & X meets Z;

theorem :: BOOLEALG:32
X meets Y \ Z implies X meets Y;

theorem :: BOOLEALG:33
X misses Bottom L;

theorem :: BOOLEALG:34
X misses Z & Y [= Z implies X misses Y;

theorem :: BOOLEALG:35
X misses Y or X misses Z implies X misses Y "/\" Z;

theorem :: BOOLEALG:36
X [= Y & X [= Z & Y misses Z implies X = Bottom L;

theorem :: BOOLEALG:37
X misses Y implies (Z "/\" X) misses (Z "/\" Y)
& (X "/\" Z) misses (Y "/\" Z);

begin   ::Boolean Lattices

reserve L for B_Lattice;
reserve X,Y,Z,V for Element of L;

theorem :: BOOLEALG:38
X \ Y [= Z implies X [= Y "\/" Z;

theorem :: BOOLEALG:39
X [= Y implies Z \ Y [= Z \ X;

theorem :: BOOLEALG:40
X [= Y & Z [= V implies X \ V [= Y \ Z;

theorem :: BOOLEALG:41
X [= Y "\/" Z implies X \ Y [= Z & X \ Z [= Y;

theorem :: BOOLEALG:42
X` [= (X "/\" Y)` & Y` [= (X "/\" Y)`;

theorem :: BOOLEALG:43
(X "\/" Y)` [= X` & (X "\/" Y)` [= Y`;

theorem :: BOOLEALG:44
X [= Y \ X implies X = Bottom L;

theorem :: BOOLEALG:45
X [= Y implies Y = X "\/" (Y \ X);

theorem :: BOOLEALG:46
X \ Y = Bottom L iff X [= Y;

theorem :: BOOLEALG:47
X [= (Y "\/" Z) & X "/\" Z = Bottom L implies X [= Y;

theorem :: BOOLEALG:48
X "\/" Y = (X \ Y) "\/" Y;

theorem :: BOOLEALG:49
X \ (X "\/" Y) = Bottom L;

theorem :: BOOLEALG:50
X \ X "/\" Y = X \ Y & X \ Y "/\" X = X \ Y;

theorem :: BOOLEALG:51
(X \ Y) "/\" Y = Bottom L;

theorem :: BOOLEALG:52
X "\/" (Y \ X) = X "\/" Y & (Y \ X) "\/" X = Y "\/" X;

theorem :: BOOLEALG:53
(X "/\" Y) "\/" (X \ Y) = X;

theorem :: BOOLEALG:54
X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z);

theorem :: BOOLEALG:55
X \ (X \ Y) = X "/\" Y;

theorem :: BOOLEALG:56
(X "\/" Y) \ Y = X \ Y;

theorem :: BOOLEALG:57
X "/\" Y = Bottom L iff X \ Y = X;

theorem :: BOOLEALG:58
X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z);

theorem :: BOOLEALG:59
X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z);

theorem :: BOOLEALG:60
X "/\" (Y \ Z) = X "/\" Y \ X "/\" Z & (Y \ Z) "/\" X = Y "/\" X \ Z "/\" X
;

theorem :: BOOLEALG:61
(X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X);

theorem :: BOOLEALG:62
(X \ Y) \ Z = X \ (Y "\/" Z);

theorem :: BOOLEALG:63
X \ Y = Y \ X implies X = Y;

canceled 2;

theorem :: BOOLEALG:66
X \ X = Bottom L;

theorem :: BOOLEALG:67
X \ Bottom L = X;

theorem :: BOOLEALG:68
(X \ Y)` = X` "\/" Y;

theorem :: BOOLEALG:69
X meets Y "\/" Z iff X meets Y or X meets Z;

theorem :: BOOLEALG:70
X "/\" Y misses X \ Y;

theorem :: BOOLEALG:71
X misses Y "\/" Z iff X misses Y & X misses Z;

theorem :: BOOLEALG:72
(X \ Y) misses Y;

theorem :: BOOLEALG:73
X misses Y implies (X "\/" Y) \ Y = X & (X "\/" Y) \ X = Y;

theorem :: BOOLEALG:74
X` "\/" Y` = X "\/" Y & X misses X` & Y misses Y` implies
X = Y` & Y = X`;

theorem :: BOOLEALG:75
X` "\/" Y` = X "\/" Y & Y misses X` & X misses Y`
implies X = X` & Y = Y`;

theorem :: BOOLEALG:76
X \+\ Bottom L = X;

theorem :: BOOLEALG:77
X \+\ X = Bottom L;

theorem :: BOOLEALG:78
X "/\" Y misses X \+\ Y;

theorem :: BOOLEALG:79
X "\/" Y = X \+\ (Y \ X);

theorem :: BOOLEALG:80
X \+\ (X "/\" Y) = X \ Y;

theorem :: BOOLEALG:81
X "\/" Y = (X \+\ Y) "\/" (X "/\" Y);

theorem :: BOOLEALG:82
(X \+\ Y) \+\ (X "/\" Y) = X "\/" Y;

theorem :: BOOLEALG:83
(X \+\ Y) \+\ (X "\/" Y) = X "/\" Y;

theorem :: BOOLEALG:84
X \+\ Y = (X "\/" Y) \ (X "/\" Y);

theorem :: BOOLEALG:85
(X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z));

theorem :: BOOLEALG:86
X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" (X "/\" Y "/\" Z);

theorem :: BOOLEALG:87
(X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);

theorem :: BOOLEALG:88
(X \+\ Y)` = (X "/\" Y) "\/" (X` "/\" Y`);
```