:: Boolean Properties of Lattices
:: by Agnieszka Julia Marasik
::
:: Received March 28, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

definition
let L be Lattice;
let X, Y be Element of L;
func X \ Y -> Element of L equals :: BOOLEALG:def 1
X "/\" (Y `);
coherence
X "/\" (Y `) is Element of L ;
end;

:: deftheorem defines \ BOOLEALG:def 1 :
for L being Lattice
for X, Y being Element of L holds X \ Y = X "/\" (Y `);

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

:: deftheorem defines \+\ BOOLEALG:def 2 :
for L being Lattice
for X, Y being Element of L holds X \+\ Y = (X \ Y) "\/" (Y \ X);

definition
let L be Lattice;
let X, Y be Element of L;
:: original: =
redefine pred X = Y means :Def3: :: BOOLEALG:def 3
( X [= Y & Y [= X );
compatibility
( X = Y iff ( X [= Y & Y [= X ) ) by LATTICES:8;
end;

:: deftheorem Def3 defines = BOOLEALG:def 3 :
for L being Lattice
for X, Y being Element of L holds
( X = Y iff ( X [= Y & Y [= X ) );

definition
let L be Lattice;
let X, Y be Element of L;
pred X meets Y means :Def4: :: BOOLEALG:def 4
X "/\" Y <> Bottom L;
end;

:: deftheorem Def4 defines meets BOOLEALG:def 4 :
for L being Lattice
for X, Y being Element of L holds
( X meets Y iff X "/\" Y <> Bottom L );

notation
let L be Lattice;
let X, Y be Element of L;
antonym X misses Y for X meets Y;
end;

theorem :: BOOLEALG:1
for L being Lattice
for X, Y, Z being Element of L st X "\/" Y [= Z holds
X [= Z
proof end;

theorem :: BOOLEALG:2
for L being Lattice
for X, Y, Z being Element of L holds X "/\" Y [= X "\/" Z
proof end;

theorem :: BOOLEALG:3
for L being Lattice
for X, Z, Y being Element of L st X [= Z holds
X \ Y [= Z
proof end;

theorem :: BOOLEALG:4
for L being Lattice
for X, Y, Z being Element of L st X \ Y [= Z & Y \ X [= Z holds
X \+\ Y [= Z by FILTER_0:6;

theorem :: BOOLEALG:5
for L being Lattice
for X, Y, Z being Element of L holds
( X = Y "\/" Z iff ( Y [= X & Z [= X & ( for V being Element of L st Y [= V & Z [= V holds
X [= V ) ) )
proof end;

theorem :: BOOLEALG:6
for L being Lattice
for X, Y, Z being Element of L holds
( X = Y "/\" Z iff ( X [= Y & X [= Z & ( for V being Element of L st V [= Y & V [= Z holds
V [= X ) ) )
proof end;

Lm1: for L being Lattice
for X, Y being Element of L st X meets Y holds
Y meets X
proof end;

theorem :: BOOLEALG:7
for L being Lattice
for X being Element of L holds
( X meets X iff X <> Bottom L )
proof end;

definition
let L be Lattice;
let X, Y be Element of L;
:: original: meets
redefine pred X meets Y;
symmetry
for X, Y being Element of L st (L,b1,b2) holds
(L,b2,b1) by Lm1;
:: original: \+\
redefine func X \+\ Y -> Element of L;
commutativity
for X, Y being Element of L holds X \+\ Y = Y \+\ X ;
:: original: meets
redefine pred X misses Y;
symmetry
for X, Y being Element of L st (L,b1,b2) holds
not (L,b2,b1) by Lm1;
end;

begin

begin

theorem :: BOOLEALG:8
for L being D_Lattice
for X, Y, Z being Element of L st (X "/\" Y) "\/" (X "/\" Z) = X holds
X [= Y "\/" Z
proof end;

begin

theorem Th9: :: BOOLEALG:9
for L being 0_Lattice
for X being Element of L st X [= Bottom L holds
X = Bottom L
proof end;

theorem :: BOOLEALG:10
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & X [= Z & Y "/\" Z = Bottom L holds
X = Bottom L by Th9, FILTER_0:7;

theorem Th11: :: BOOLEALG:11
for L being 0_Lattice
for X, Y being Element of L holds
( X "\/" Y = Bottom L iff ( X = Bottom L & Y = Bottom L ) )
proof end;

theorem :: BOOLEALG:12
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & Y "/\" Z = Bottom L holds
X "/\" Z = Bottom L by LATTICES:9, Th9;

theorem Th13: :: BOOLEALG:13
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y & Y [= Z holds
X meets Z
proof end;

theorem Th14: :: BOOLEALG:14
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y "/\" Z holds
( X meets Y & X meets Z )
proof end;

theorem :: BOOLEALG:15
for L being 0_Lattice
for X, Y, Z being Element of L st X meets Y \ Z holds
X meets Y
proof end;

theorem :: BOOLEALG:16
for L being 0_Lattice
for X being Element of L holds X misses Bottom L
proof end;

theorem :: BOOLEALG:17
for L being 0_Lattice
for X, Z, Y being Element of L st X misses Z & Y [= Z holds
X misses Y by Th13;

theorem :: BOOLEALG:18
for L being 0_Lattice
for X, Y, Z being Element of L st ( X misses Y or X misses Z ) holds
X misses Y "/\" Z by Th14;

theorem :: BOOLEALG:19
for L being 0_Lattice
for X, Y, Z being Element of L st X [= Y & X [= Z & Y misses Z holds
X = Bottom L
proof end;

theorem :: BOOLEALG:20
for L being 0_Lattice
for X, Y, Z being Element of L st X misses Y holds
Z "/\" X misses Z "/\" Y
proof end;

begin

theorem :: BOOLEALG:21
for L being B_Lattice
for X, Y, Z being Element of L st X \ Y [= Z holds
X [= Y "\/" Z
proof end;

theorem Th22: :: BOOLEALG:22
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y holds
Z \ Y [= Z \ X
proof end;

theorem :: BOOLEALG:23
for L being B_Lattice
for X, Y, Z, V being Element of L st X [= Y & Z [= V holds
X \ V [= Y \ Z
proof end;

theorem :: BOOLEALG:24
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y "\/" Z holds
X \ Y [= Z
proof end;

theorem :: BOOLEALG:25
for L being B_Lattice
for X, Y being Element of L holds X ` [= (X "/\" Y) `
proof end;

theorem :: BOOLEALG:26
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) ` [= X `
proof end;

theorem :: BOOLEALG:27
for L being B_Lattice
for X, Y being Element of L st X [= Y \ X holds
X = Bottom L
proof end;

theorem :: BOOLEALG:28
for L being B_Lattice
for X, Y being Element of L st X [= Y holds
Y = X "\/" (Y \ X)
proof end;

theorem Th29: :: BOOLEALG:29
for L being B_Lattice
for X, Y being Element of L holds
( X \ Y = Bottom L iff X [= Y )
proof end;

theorem :: BOOLEALG:30
for L being B_Lattice
for X, Y, Z being Element of L st X [= Y "\/" Z & X "/\" Z = Bottom L holds
X [= Y
proof end;

theorem :: BOOLEALG:31
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = (X \ Y) "\/" Y
proof end;

theorem :: BOOLEALG:32
for L being B_Lattice
for X, Y being Element of L holds X \ (X "\/" Y) = Bottom L by Th29, LATTICES:5;

theorem Th33: :: BOOLEALG:33
for L being B_Lattice
for X, Y being Element of L holds X \ (X "/\" Y) = X \ Y
proof end;

theorem :: BOOLEALG:34
for L being B_Lattice
for X, Y being Element of L holds (X \ Y) "/\" Y = Bottom L
proof end;

theorem Th35: :: BOOLEALG:35
for L being B_Lattice
for X, Y being Element of L holds X "\/" (Y \ X) = X "\/" Y
proof end;

theorem Th36: :: BOOLEALG:36
for L being B_Lattice
for X, Y being Element of L holds (X "/\" Y) "\/" (X \ Y) = X
proof end;

theorem Th37: :: BOOLEALG:37
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)
proof end;

theorem :: BOOLEALG:38
for L being B_Lattice
for X, Y being Element of L holds X \ (X \ Y) = X "/\" Y
proof end;

theorem :: BOOLEALG:39
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ Y = X \ Y
proof end;

theorem :: BOOLEALG:40
for L being B_Lattice
for X, Y being Element of L holds
( X "/\" Y = Bottom L iff X \ Y = X )
proof end;

theorem :: BOOLEALG:41
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z)
proof end;

theorem Th42: :: BOOLEALG:42
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z)
proof end;

theorem :: BOOLEALG:43
for L being B_Lattice
for X, Y, Z being Element of L holds X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z)
proof end;

theorem Th44: :: BOOLEALG:44
for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)
proof end;

theorem Th45: :: BOOLEALG:45
for L being B_Lattice
for X, Y, Z being Element of L holds (X \ Y) \ Z = X \ (Y "\/" Z)
proof end;

theorem :: BOOLEALG:46
for L being B_Lattice
for X, Y being Element of L st X \ Y = Y \ X holds
X = Y
proof end;

theorem Th47: :: BOOLEALG:47
for L being B_Lattice
for X being Element of L holds X \ (Bottom L) = X
proof end;

theorem :: BOOLEALG:48
for L being B_Lattice
for X, Y being Element of L holds (X \ Y) ` = (X `) "\/" Y
proof end;

theorem Th49: :: BOOLEALG:49
for L being B_Lattice
for X, Y, Z being Element of L holds
( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )
proof end;

theorem Th50: :: BOOLEALG:50
for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \ Y
proof end;

theorem :: BOOLEALG:51
for L being B_Lattice
for X, Y, Z being Element of L holds
( X misses Y "\/" Z iff ( X misses Y & X misses Z ) ) by Th49;

theorem :: BOOLEALG:52
for L being B_Lattice
for X, Y being Element of L holds X \ Y misses Y
proof end;

theorem :: BOOLEALG:53
for L being B_Lattice
for X, Y being Element of L st X misses Y holds
(X "\/" Y) \ Y = X
proof end;

theorem :: BOOLEALG:54
for L being B_Lattice
for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & X misses X ` & Y misses Y ` holds
( X = Y ` & Y = X ` )
proof end;

theorem :: BOOLEALG:55
for L being B_Lattice
for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & Y misses X ` & X misses Y ` holds
( X = X ` & Y = Y ` )
proof end;

theorem :: BOOLEALG:56
for L being B_Lattice
for X being Element of L holds X \+\ (Bottom L) = X
proof end;

theorem :: BOOLEALG:57
for L being B_Lattice
for X being Element of L holds X \+\ X = Bottom L by LATTICES:20;

theorem :: BOOLEALG:58
for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \+\ Y
proof end;

theorem :: BOOLEALG:59
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = X \+\ (Y \ X)
proof end;

theorem :: BOOLEALG:60
for L being B_Lattice
for X, Y being Element of L holds X \+\ (X "/\" Y) = X \ Y
proof end;

theorem :: BOOLEALG:61
for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = (X \+\ Y) "\/" (X "/\" Y)
proof end;

Lm2: for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X \+\ Y) = X "/\" Y
proof end;

theorem :: BOOLEALG:62
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y
proof end;

theorem :: BOOLEALG:63
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y
proof end;

theorem Th64: :: BOOLEALG:64
for L being B_Lattice
for X, Y being Element of L holds X \+\ Y = (X "\/" Y) \ (X "/\" Y)
proof end;

theorem :: BOOLEALG:65
for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z))
proof end;

theorem :: BOOLEALG:66
for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)
proof end;

theorem :: BOOLEALG:67
for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)
proof end;

theorem :: BOOLEALG:68
for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) ` = (X "/\" Y) "\/" ((X `) "/\" (Y `))
proof end;