The abstract of the Mizar article:

Boolean Properties of Lattices

by

Agnieszka Julia Marasik

Received March 28, 1994

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