:: by Agnieszka Julia Marasik

::

:: Received November 8, 1996

:: Copyright (c) 1996-2021 Association of Mizar Users

theorem :: YELLOW_5:3

for L being transitive antisymmetric with_suprema RelStr

for a, b, c being Element of L st a "\/" b <= c holds

a <= c

for a, b, c being Element of L st a "\/" b <= c holds

a <= c

proof end;

theorem :: YELLOW_5:4

for L being transitive antisymmetric with_infima RelStr

for a, b, c being Element of L st c <= a "/\" b holds

c <= a

for a, b, c being Element of L st c <= a "/\" b holds

c <= a

proof end;

theorem :: YELLOW_5:5

for L being transitive antisymmetric with_suprema with_infima RelStr

for a, b, c being Element of L holds a "/\" b <= a "\/" c

for a, b, c being Element of L holds a "/\" b <= a "\/" c

proof end;

theorem Th6: :: YELLOW_5:6

for L being transitive antisymmetric with_infima RelStr

for a, b, c being Element of L st a <= b holds

a "/\" c <= b "/\" c

for a, b, c being Element of L st a <= b holds

a "/\" c <= b "/\" c

proof end;

theorem Th7: :: YELLOW_5:7

for L being transitive antisymmetric with_suprema RelStr

for a, b, c being Element of L st a <= b holds

a "\/" c <= b "\/" c

for a, b, c being Element of L st a <= b holds

a "\/" c <= b "\/" c

proof end;

theorem Th11: :: YELLOW_5:11

for L being Boolean LATTICE

for x, y being Element of L holds

( y is_a_complement_of x iff y = 'not' x )

for x, y being Element of L holds

( y is_a_complement_of x iff y = 'not' x )

proof end;

definition

let L be non empty RelStr ;

let a, b be Element of L;

correctness

coherence

a "/\" ('not' b) is Element of L;

;

end;
let a, b be Element of L;

correctness

coherence

a "/\" ('not' b) is Element of L;

;

:: deftheorem defines \ YELLOW_5:def 1 :

for L being non empty RelStr

for a, b being Element of L holds a \ b = a "/\" ('not' b);

for L being non empty RelStr

for a, b being Element of L holds a \ b = a "/\" ('not' b);

definition

let L be non empty RelStr ;

let a, b be Element of L;

correctness

coherence

(a \ b) "\/" (b \ a) is Element of L;

;

end;
let a, b be Element of L;

correctness

coherence

(a \ b) "\/" (b \ a) is Element of L;

;

:: deftheorem defines \+\ YELLOW_5:def 2 :

for L being non empty RelStr

for a, b being Element of L holds a \+\ b = (a \ b) "\/" (b \ a);

for L being non empty RelStr

for a, b being Element of L holds a \+\ b = (a \ b) "\/" (b \ a);

definition

let L be antisymmetric with_suprema with_infima RelStr ;

let a, b be Element of L;

:: original: \+\

redefine func a \+\ b -> Element of L;

commutativity

for a, b being Element of L holds a \+\ b = b \+\ a

end;
let a, b be Element of L;

:: original: \+\

redefine func a \+\ b -> Element of L;

commutativity

for a, b being Element of L holds a \+\ b = b \+\ a

proof end;

:: deftheorem defines meets YELLOW_5:def 3 :

for L being non empty RelStr

for a, b being Element of L holds

( a meets b iff a "/\" b <> Bottom L );

for L being non empty RelStr

for a, b being Element of L holds

( a meets b iff a "/\" b <> Bottom L );

notation

let L be antisymmetric with_infima RelStr ;

let a, b be Element of L;

antonym a misses b for a meets b;

end;
let a, b be Element of L;

antonym a misses b for a meets b;

definition

let L be antisymmetric with_infima RelStr ;

let a, b be Element of L;

:: original: meets

redefine pred a meets b;

symmetry

for a, b being Element of L st (L,b_{1},b_{2}) holds

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

end;
let a, b be Element of L;

:: original: meets

redefine pred a meets b;

symmetry

for a, b being Element of L st (L,b

(L,b

proof end;

theorem :: YELLOW_5:12

for L being transitive antisymmetric with_suprema with_infima RelStr

for a, b, c being Element of L st a <= c holds

a \ b <= c

for a, b, c being Element of L st a <= c holds

a \ b <= c

proof end;

theorem :: YELLOW_5:13

for L being transitive antisymmetric with_suprema with_infima RelStr

for a, b, c being Element of L st a <= b holds

a \ c <= b \ c by Th6;

for a, b, c being Element of L st a <= b holds

a \ c <= b \ c by Th6;

theorem :: YELLOW_5:14

theorem :: YELLOW_5:15

theorem :: YELLOW_5:16

for L being transitive antisymmetric with_infima RelStr st L is distributive holds

for a, b, c being Element of L st (a "/\" b) "\/" (a "/\" c) = a holds

a <= b "\/" c

for a, b, c being Element of L st (a "/\" b) "\/" (a "/\" c) = a holds

a <= b "\/" c

proof end;

theorem Th17: :: YELLOW_5:17

for L being LATTICE st L is distributive holds

for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)

for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)

proof end;

theorem :: YELLOW_5:18

for L being LATTICE st L is distributive holds

for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c)

for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c)

proof end;

theorem Th19: :: YELLOW_5:19

for L being non empty antisymmetric lower-bounded RelStr

for a being Element of L st a <= Bottom L holds

a = Bottom L

for a being Element of L st a <= Bottom L holds

a = Bottom L

proof end;

theorem :: YELLOW_5:20

for L being lower-bounded Semilattice

for a, b, c being Element of L st a <= b & a <= c & b "/\" c = Bottom L holds

a = Bottom L

for a, b, c being Element of L st a <= b & a <= c & b "/\" c = Bottom L holds

a = Bottom L

proof end;

theorem :: YELLOW_5:21

for L being antisymmetric with_suprema lower-bounded RelStr

for a, b being Element of L st a "\/" b = Bottom L holds

( a = Bottom L & b = Bottom L )

for a, b being Element of L st a "\/" b = Bottom L holds

( a = Bottom L & b = Bottom L )

proof end;

theorem :: YELLOW_5:22

for L being transitive antisymmetric with_infima lower-bounded RelStr

for a, b, c being Element of L st a <= b & b "/\" c = Bottom L holds

a "/\" c = Bottom L

for a, b, c being Element of L st a <= b & b "/\" c = Bottom L holds

a "/\" c = Bottom L

proof end;

theorem :: YELLOW_5:24

for L being transitive antisymmetric with_infima lower-bounded RelStr

for a, b, c being Element of L st a meets b & b <= c holds

a meets c

for a, b, c being Element of L st a meets b & b <= c holds

a meets c

proof end;

theorem Th25: :: YELLOW_5:25

for L being antisymmetric with_infima lower-bounded RelStr

for a being Element of L holds a "/\" (Bottom L) = Bottom L

for a being Element of L holds a "/\" (Bottom L) = Bottom L

proof end;

theorem :: YELLOW_5:26

for L being transitive antisymmetric with_suprema with_infima lower-bounded RelStr

for a, b, c being Element of L st a meets b "/\" c holds

a meets b

for a, b, c being Element of L st a meets b "/\" c holds

a meets b

proof end;

theorem :: YELLOW_5:27

for L being transitive antisymmetric with_suprema with_infima lower-bounded RelStr

for a, b, c being Element of L st a meets b \ c holds

a meets b

for a, b, c being Element of L st a meets b \ c holds

a meets b

proof end;

theorem :: YELLOW_5:28

for L being transitive antisymmetric with_infima lower-bounded RelStr

for a being Element of L holds a misses Bottom L by Th25;

for a being Element of L holds a misses Bottom L by Th25;

theorem :: YELLOW_5:29

for L being transitive antisymmetric with_infima lower-bounded RelStr

for a, b, c being Element of L st a misses c & b <= c holds

a misses b

for a, b, c being Element of L st a misses c & b <= c holds

a misses b

proof end;

theorem :: YELLOW_5:30

for L being transitive antisymmetric with_infima lower-bounded RelStr

for a, b, c being Element of L st ( a misses b or a misses c ) holds

a misses b "/\" c

for a, b, c being Element of L st ( a misses b or a misses c ) holds

a misses b "/\" c

proof end;

theorem :: YELLOW_5:31

for L being lower-bounded LATTICE

for a, b, c being Element of L st a <= b & a <= c & b misses c holds

a = Bottom L

for a, b, c being Element of L st a <= b & a <= c & b misses c holds

a = Bottom L

proof end;

theorem :: YELLOW_5:32

for L being transitive antisymmetric with_infima lower-bounded RelStr

for a, b, c being Element of L st a misses b holds

a "/\" c misses b "/\" c

for a, b, c being Element of L st a misses b holds

a "/\" c misses b "/\" c

proof end;

theorem :: YELLOW_5:33

for L being non empty Boolean RelStr

for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)

for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a)

proof end;

theorem Th34: :: YELLOW_5:34

for L being non empty Boolean RelStr

for a being Element of L holds

( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )

for a being Element of L holds

( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )

proof end;

theorem :: YELLOW_5:35

for L being non empty Boolean RelStr

for a, b, c being Element of L st a \ b <= c holds

a <= b "\/" c

for a, b, c being Element of L st a \ b <= c holds

a <= b "\/" c

proof end;

theorem Th36: :: YELLOW_5:36

for L being non empty Boolean RelStr

for a, b being Element of L holds

( 'not' (a "\/" b) = ('not' a) "/\" ('not' b) & 'not' (a "/\" b) = ('not' a) "\/" ('not' b) )

for a, b being Element of L holds

( 'not' (a "\/" b) = ('not' a) "/\" ('not' b) & 'not' (a "/\" b) = ('not' a) "\/" ('not' b) )

proof end;

theorem :: YELLOW_5:39

for L being non empty Boolean RelStr

for a, b, c, d being Element of L st a <= b & c <= d holds

a \ d <= b \ c

for a, b, c, d being Element of L st a <= b & c <= d holds

a \ d <= b \ c

proof end;

theorem :: YELLOW_5:40

for L being non empty Boolean RelStr

for a, b, c being Element of L st a <= b "\/" c holds

( a \ b <= c & a \ c <= b )

for a, b, c being Element of L st a <= b "\/" c holds

( a \ b <= c & a \ c <= b )

proof end;

theorem :: YELLOW_5:41

for L being non empty Boolean RelStr

for a, b being Element of L holds

( 'not' a <= 'not' (a "/\" b) & 'not' b <= 'not' (a "/\" b) )

for a, b being Element of L holds

( 'not' a <= 'not' (a "/\" b) & 'not' b <= 'not' (a "/\" b) )

proof end;

theorem :: YELLOW_5:42

for L being non empty Boolean RelStr

for a, b being Element of L holds

( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b )

for a, b being Element of L holds

( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b )

proof end;

theorem :: YELLOW_5:45

for L being non empty Boolean RelStr

for a, b being Element of L holds

( a \ b = Bottom L iff a <= b )

for a, b being Element of L holds

( a \ b = Bottom L iff a <= b )

proof end;

theorem :: YELLOW_5:46

for L being non empty Boolean RelStr

for a, b, c being Element of L st a <= b "\/" c & a "/\" c = Bottom L holds

a <= b

for a, b, c being Element of L st a <= b "\/" c & a "/\" c = Bottom L holds

a <= b

proof end;

theorem :: YELLOW_5:53

for L being non empty Boolean RelStr

for a, b, c being Element of L holds a \ (b \ c) = (a \ b) "\/" (a "/\" c)

for a, b, c being Element of L holds a \ (b \ c) = (a \ b) "\/" (a "/\" c)

proof end;

theorem :: YELLOW_5:56

for L being non empty Boolean RelStr

for a, b being Element of L holds

( a "/\" b = Bottom L iff a \ b = a )

for a, b being Element of L holds

( a "/\" b = Bottom L iff a \ b = a )

proof end;

theorem :: YELLOW_5:57

for L being non empty Boolean RelStr

for a, b, c being Element of L holds a \ (b "\/" c) = (a \ b) "/\" (a \ c)

for a, b, c being Element of L holds a \ (b "\/" c) = (a \ b) "/\" (a \ c)

proof end;

theorem :: YELLOW_5:58

for L being non empty Boolean RelStr

for a, b, c being Element of L holds a \ (b "/\" c) = (a \ b) "\/" (a \ c)

for a, b, c being Element of L holds a \ (b "/\" c) = (a \ b) "\/" (a \ c)

proof end;

theorem :: YELLOW_5:59

for L being non empty Boolean RelStr

for a, b, c being Element of L holds a "/\" (b \ c) = (a "/\" b) \ (a "/\" c)

for a, b, c being Element of L holds a "/\" (b \ c) = (a "/\" b) \ (a "/\" c)

proof end;

theorem :: YELLOW_5:60

for L being non empty Boolean RelStr

for a, b being Element of L holds (a "\/" b) \ (a "/\" b) = (a \ b) "\/" (b \ a)

for a, b being Element of L holds (a "\/" b) \ (a "/\" b) = (a \ b) "\/" (b \ a)

proof end;

theorem :: YELLOW_5:61

for L being non empty Boolean RelStr

for a, b, c being Element of L holds (a \ b) \ c = a \ (b "\/" c)

for a, b, c being Element of L holds (a \ b) \ c = a \ (b "\/" c)

proof end;

theorem :: YELLOW_5:64

theorem :: YELLOW_5:66

for L being non empty Boolean RelStr

for a, b being Element of L holds 'not' (a \ b) = ('not' a) "\/" b

for a, b being Element of L holds 'not' (a \ b) = ('not' a) "\/" b

proof end;

theorem :: YELLOW_5:69

for L being non empty Boolean RelStr

for a, b being Element of L st a misses b holds

(a "\/" b) \ b = a

for a, b being Element of L st a misses b holds

(a "\/" b) \ b = a

proof end;