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

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 :: BOOLEALG:def 3
( X [= Y & Y [= X );

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

end;

:: deftheorem 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 :: BOOLEALG:def 4
X "/\" Y <> Bottom L;

end;

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

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, Y, Z 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;

theorem :: BOOLEALG:7

for L being Lattice
for X being Element of L holds
( X meets X iff X <> Bottom L ) ;

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₁,b₂) holds
(L,b₂,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₁,b₂) holds
not (L,b₂,b₁) ;

end;

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;

theorem Th9: :: BOOLEALG:9

for L being 0_Lattice
for X being Element of L st X [= Bottom L holds
X = Bottom L by LATTICES:16;

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 ) ) by LATTICES:5, LATTICES:16;

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 Th9, LATTICES:9;

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 by Th9, LATTICES:9;

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 ;

theorem :: BOOLEALG:17

for L being 0_Lattice
for X, Y, Z 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 by Th9, FILTER_0:7;

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;

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 by Th47;

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;

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