:: by Agnieszka Julia Marasik

::

:: Received March 28, 1994

:: Copyright (c) 1994-2018 Association of Mizar Users

:: deftheorem defines \ BOOLEALG:def 1 :

for L being Lattice

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

for L being Lattice

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

definition
end;

:: deftheorem defines \+\ BOOLEALG:def 2 :

for L being Lattice

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

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;

compatibility

( X = Y iff ( X [= Y & Y [= X ) ) by LATTICES:8;

end;
let X, Y be Element of L;

compatibility

( X = Y iff ( X [= Y & Y [= X ) ) by LATTICES:8;

:: deftheorem defines = BOOLEALG:def 3 :

for L being Lattice

for X, Y being Element of L holds

( X = Y iff ( X [= Y & Y [= X ) );

for L being Lattice

for X, Y being Element of L holds

( X = Y iff ( X [= Y & Y [= X ) );

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

for L being Lattice

for X, Y being Element of L holds

( X meets Y iff X "/\" Y <> Bottom L );

theorem :: BOOLEALG:4

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

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

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;

theorem :: BOOLEALG:7

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,b_{1},b_{2}) holds

(L,b_{2},b_{1})
;

:: 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,b_{1},b_{2}) holds

not (L,b_{2},b_{1})
;

end;
let X, Y be Element of L;

:: original: meets

redefine pred X meets Y;

symmetry

for X, Y being Element of L st (L,b

(L,b

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

not (L,b

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

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

X [= Y "\/" Z

proof end;

theorem :: BOOLEALG:10

theorem :: BOOLEALG:12

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 )

for X, Y, Z being Element of L st X meets Y "/\" Z holds

( X meets Y & X meets Z )

proof end;

theorem :: BOOLEALG:17

theorem :: BOOLEALG:18

theorem :: BOOLEALG:19

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

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

X [= Y

proof end;

theorem :: BOOLEALG:32

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)

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

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

for X, Y, Z being Element of L holds

( X meets Y "\/" Z iff ( X meets Y or X meets Z ) )

proof end;

theorem :: BOOLEALG:51

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

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

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

theorem :: BOOLEALG:57

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

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)

for X, Y, Z being Element of L holds X \ (Y \+\ Z) = (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 `))

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

proof end;