:: Miscellaneous Facts about Relation Structure
:: by Agnieszka Julia Marasik
::
:: Received November 8, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

theorem :: YELLOW_5:1

for L being reflexive antisymmetric with_suprema RelStr
for a being Element of L holds a "\/" a = a

proof end;

theorem Th2: :: YELLOW_5:2

for L being reflexive antisymmetric with_infima RelStr
for a being Element of L holds a "/\" a = a

proof end;

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

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

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

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

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

proof end;

theorem Th8: :: YELLOW_5:8

for L being sup-Semilattice
for a, b being Element of L st a <= b holds
a "\/" b = b

proof end;

theorem Th9: :: YELLOW_5:9

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

proof end;

theorem Th10: :: YELLOW_5:10

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

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 )

proof end;

definition

let L be non empty RelStr ;
let a, b be Element of L;

func a \ b -> Element of L equals :: YELLOW_5:def 1
a "/\" ('not' b);

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

end;

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

definition

let L be non empty RelStr ;
let a, b be Element of L;

func a \+\ b -> Element of L equals :: YELLOW_5:def 2
(a \ b) "\/" (b \ a);

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

end;

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

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

proof end;

end;

definition

let L be non empty RelStr ;
let a, b be Element of L;

pred a meets b means :: YELLOW_5:def 3
a "/\" b <> Bottom L;

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

notation

let L be non empty RelStr ;
let a, b be Element of L;
antonym a misses b for a meets b;

end;

notation

let L be antisymmetric with_infima RelStr ;
let a, b be Element of L;
antonym a misses b for a meets b;

end;

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

proof end;

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

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;

theorem :: YELLOW_5:14

for L being LATTICE
for a, b, c being Element of L st a \ b <= c & b \ a <= c holds
a \+\ b <= c by Th9;

theorem :: YELLOW_5:15

for L being LATTICE
for a being Element of L holds
( a meets a iff a <> Bottom L ) by Th2;

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

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)

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)

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

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

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 )

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

proof end;

theorem :: YELLOW_5:23

for L being lower-bounded Semilattice
for a being Element of L holds (Bottom L) \ a = 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

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

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

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

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;

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

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

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

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

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)

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 )

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

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

proof end;

theorem Th37: :: YELLOW_5:37

for L being non empty Boolean RelStr
for a, b being Element of L st a <= b holds
'not' b <= 'not' a

proof end;

theorem :: YELLOW_5:38

for L being non empty Boolean RelStr
for a, b, c being Element of L st a <= b holds
c \ b <= c \ a

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

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 )

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

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 )

proof end;

theorem :: YELLOW_5:43

for L being non empty Boolean RelStr
for a, b being Element of L st a <= b \ a holds
a = Bottom L

proof end;

theorem :: YELLOW_5:44

for L being non empty Boolean RelStr
for a, b being Element of L st a <= b holds
b = a "\/" (b \ a)

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 )

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

proof end;

theorem :: YELLOW_5:47

for L being non empty Boolean RelStr
for a, b being Element of L holds a "\/" b = (a \ b) "\/" b

proof end;

theorem :: YELLOW_5:48

for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a "\/" b) = Bottom L

proof end;

theorem :: YELLOW_5:49

for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a "/\" b) = a \ b

proof end;

theorem :: YELLOW_5:50

for L being non empty Boolean RelStr
for a, b being Element of L holds (a \ b) "/\" b = Bottom L

proof end;

theorem :: YELLOW_5:51

for L being non empty Boolean RelStr
for a, b being Element of L holds a "\/" (b \ a) = a "\/" b

proof end;

theorem :: YELLOW_5:52

for L being non empty Boolean RelStr
for a, b being Element of L holds (a "/\" b) "\/" (a \ b) = a

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)

proof end;

theorem :: YELLOW_5:54

for L being non empty Boolean RelStr
for a, b being Element of L holds a \ (a \ b) = a "/\" b

proof end;

theorem :: YELLOW_5:55

for L being non empty Boolean RelStr
for a, b being Element of L holds (a "\/" b) \ b = a \ b

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 )

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)

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)

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)

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)

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)

proof end;

theorem Th62: :: YELLOW_5:62

for L being non empty Boolean RelStr holds 'not' (Bottom L) = Top L

proof end;

theorem :: YELLOW_5:63

for L being non empty Boolean RelStr holds 'not' (Top L) = Bottom L

proof end;

theorem :: YELLOW_5:64

for L being non empty Boolean RelStr
for a being Element of L holds a \ a = Bottom L by Th34;

theorem :: YELLOW_5:65

for L being non empty Boolean RelStr
for a being Element of L holds a \ (Bottom L) = a

proof end;

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

proof end;

theorem :: YELLOW_5:67

for L being non empty Boolean RelStr
for a, b being Element of L holds a "/\" b misses a \ b

proof end;

theorem :: YELLOW_5:68

for L being non empty Boolean RelStr
for a, b being Element of L holds a \ b misses 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

proof end;