:: Boolean Properties of Lattices
:: by Agnieszka Julia Marasik
::
:: Received March 28, 1994
:: Copyright (c) 1994-2011 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:26;

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

canceled;

theorem :: BOOLEALG:2

canceled;

theorem :: BOOLEALG:3

for L being Lattice
for X, Y, Z being Element of L st X "\/" Y [= Z holds
X [= Z

proof end;

theorem :: BOOLEALG:4

for L being Lattice
for X, Y, Z being Element of L holds X "/\" Y [= X "\/" Z

proof end;

theorem :: BOOLEALG:5

canceled;

theorem :: BOOLEALG:6

for L being Lattice
for X, Z, Y being Element of L st X [= Z holds
X \ Y [= Z

proof end;

theorem :: BOOLEALG:7

canceled;

theorem :: BOOLEALG:8

canceled;

theorem :: BOOLEALG:9

canceled;

theorem :: BOOLEALG:10

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

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

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

canceled;

theorem :: BOOLEALG:14

canceled;

theorem :: BOOLEALG:15

canceled;

theorem :: BOOLEALG:16

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 X meets Y holds
Y meets X 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 not X meets Y holds
not Y meets X by Lm1;

end;

begin

begin

theorem :: BOOLEALG:17

canceled;

theorem :: BOOLEALG:18

canceled;

theorem :: BOOLEALG:19

canceled;

theorem :: BOOLEALG:20

canceled;

theorem :: BOOLEALG:21

canceled;

theorem :: BOOLEALG:22

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

canceled;

theorem :: BOOLEALG:24

canceled;

theorem Th25: :: BOOLEALG:25

for L being 0_Lattice
for X being Element of L st X [= Bottom L holds
X = Bottom L

proof end;

theorem :: BOOLEALG:26

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 Th25, FILTER_0:7;

theorem Th27: :: BOOLEALG:27

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

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 Th25, LATTICES:27;

theorem :: BOOLEALG:29

canceled;

theorem Th30: :: BOOLEALG:30

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 Th31: :: BOOLEALG:31

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

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

for L being 0_Lattice
for X being Element of L holds X misses Bottom L

proof end;

theorem :: BOOLEALG:34

for L being 0_Lattice
for X, Z, Y being Element of L st X misses Z & Y [= Z holds
X misses Y by Th30;

theorem :: BOOLEALG:35

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

theorem :: BOOLEALG:36

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

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

for L being B_Lattice
for X, Y, Z being Element of L st X \ Y [= Z holds
X [= Y "\/" Z

proof end;

theorem Th39: :: BOOLEALG:39

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

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

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

for L being B_Lattice
for X, Y being Element of L holds X ` [= (X "/\" Y) `

proof end;

theorem :: BOOLEALG:43

for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) ` [= X `

proof end;

theorem :: BOOLEALG:44

for L being B_Lattice
for X, Y being Element of L st X [= Y \ X holds
X = Bottom L

proof end;

theorem :: BOOLEALG:45

for L being B_Lattice
for X, Y being Element of L st X [= Y holds
Y = X "\/" (Y \ X)

proof end;

theorem Th46: :: BOOLEALG:46

for L being B_Lattice
for X, Y being Element of L holds
( X \ Y = Bottom L iff X [= Y )

proof end;

theorem :: BOOLEALG:47

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

for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = (X \ Y) "\/" Y

proof end;

theorem :: BOOLEALG:49

for L being B_Lattice
for X, Y being Element of L holds X \ (X "\/" Y) = Bottom L

proof end;

theorem Th50: :: BOOLEALG:50

for L being B_Lattice
for X, Y being Element of L holds X \ (X "/\" Y) = X \ Y

proof end;

theorem :: BOOLEALG:51

for L being B_Lattice
for X, Y being Element of L holds (X \ Y) "/\" Y = Bottom L

proof end;

theorem Th52: :: BOOLEALG:52

for L being B_Lattice
for X, Y being Element of L holds X "\/" (Y \ X) = X "\/" Y

proof end;

theorem Th53: :: BOOLEALG:53

for L being B_Lattice
for X, Y being Element of L holds (X "/\" Y) "\/" (X \ Y) = X

proof end;

theorem Th54: :: BOOLEALG:54

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

for L being B_Lattice
for X, Y being Element of L holds X \ (X \ Y) = X "/\" Y

proof end;

theorem :: BOOLEALG:56

for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ Y = X \ Y

proof end;

theorem :: BOOLEALG:57

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

for L being B_Lattice
for X, Y, Z being Element of L holds X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z)

proof end;

theorem Th59: :: BOOLEALG:59

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

for L being B_Lattice
for X, Y, Z being Element of L holds X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z)

proof end;

theorem Th61: :: BOOLEALG:61

for L being B_Lattice
for X, Y being Element of L holds (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)

proof end;

theorem Th62: :: BOOLEALG:62

for L being B_Lattice
for X, Y, Z being Element of L holds (X \ Y) \ Z = X \ (Y "\/" Z)

proof end;

theorem :: BOOLEALG:63

for L being B_Lattice
for X, Y being Element of L st X \ Y = Y \ X holds
X = Y

proof end;

theorem :: BOOLEALG:64

canceled;

theorem :: BOOLEALG:65

canceled;

theorem :: BOOLEALG:66

canceled;

theorem Th67: :: BOOLEALG:67

for L being B_Lattice
for X being Element of L holds X \ (Bottom L) = X

proof end;

theorem :: BOOLEALG:68

for L being B_Lattice
for X, Y being Element of L holds (X \ Y) ` = (X `) "\/" Y

proof end;

theorem Th69: :: BOOLEALG:69

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 Th70: :: BOOLEALG:70

for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \ Y

proof end;

theorem :: BOOLEALG:71

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

theorem :: BOOLEALG:72

for L being B_Lattice
for X, Y being Element of L holds X \ Y misses Y

proof end;

theorem :: BOOLEALG:73

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

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

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

for L being B_Lattice
for X being Element of L holds X \+\ (Bottom L) = X

proof end;

theorem :: BOOLEALG:77

for L being B_Lattice
for X being Element of L holds X \+\ X = Bottom L

proof end;

theorem :: BOOLEALG:78

for L being B_Lattice
for X, Y being Element of L holds X "/\" Y misses X \+\ Y

proof end;

theorem :: BOOLEALG:79

for L being B_Lattice
for X, Y being Element of L holds X "\/" Y = X \+\ (Y \ X)

proof end;

theorem :: BOOLEALG:80

for L being B_Lattice
for X, Y being Element of L holds X \+\ (X "/\" Y) = X \ Y

proof end;

theorem :: BOOLEALG:81

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

for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y

proof end;

theorem :: BOOLEALG:83

for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y

proof end;

theorem Th84: :: BOOLEALG:84

for L being B_Lattice
for X, Y being Element of L holds X \+\ Y = (X "\/" Y) \ (X "/\" Y)

proof end;

theorem :: BOOLEALG:85

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

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

for L being B_Lattice
for X, Y, Z being Element of L holds (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z)

proof end;

theorem :: BOOLEALG:88

for L being B_Lattice
for X, Y being Element of L holds (X \+\ Y) ` = (X "/\" Y) "\/" ((X `) "/\" (Y `))

proof end;