Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Miscellaneous Facts about Relation Structure

by
Agnieszka Julia Marasik

MML identifier: YELLOW_5
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_2, LATTICE3, ORDERS_1, LATTICES, WAYBEL_0, ZF_LANG, BOOLE;
notation STRUCT_0, LATTICE3, WAYBEL_0, WAYBEL_1, YELLOW_0, ORDERS_1;
constructors WAYBEL_1, LATTICE3;
clusters LATTICE3, WAYBEL_1;

begin :: Introduction

theorem :: YELLOW_5:1
for L being reflexive antisymmetric with_suprema RelStr
for a being Element of L holds
a "\/" a = a;

theorem :: YELLOW_5:2
for L being reflexive antisymmetric with_infima RelStr
for a being Element of L holds
a "/\" a = a;

theorem :: YELLOW_5:3
for L be transitive antisymmetric with_suprema RelStr
for a,b,c being Element of L holds
a"\/"b <= c implies a <= c;

theorem :: YELLOW_5:4
for L be transitive antisymmetric with_infima RelStr
for a,b,c being Element of L holds
c <= a"/\"b implies c <= a;

theorem :: YELLOW_5:5
for L be antisymmetric transitive with_suprema with_infima RelStr
for a,b,c being Element of L holds
a"/\"b <= a"\/"c;

theorem :: YELLOW_5:6
for L be antisymmetric transitive with_infima RelStr
for a,b,c be Element of L holds
a <= b implies a"/\"c <= b"/\"c;

theorem :: YELLOW_5:7
for L be antisymmetric transitive with_suprema RelStr
for a,b,c be Element of L holds
a <= b implies a"\/"c <= b"\/"c;

theorem :: YELLOW_5:8
for L be sup-Semilattice
for a,b be Element of L holds
a <= b implies a "\/" b = b;

theorem :: YELLOW_5:9
for L be sup-Semilattice
for a,b,c being Element of L holds
a <= c & b <= c implies a"\/"b <= c;

theorem :: YELLOW_5:10
for L be Semilattice
for a,b be Element of L holds
b <= a implies a"/\"b = b;

:: Difference in Relation Structure
begin

theorem :: YELLOW_5:11
for L being Boolean LATTICE, x,y being Element of L holds
y is_a_complement_of x iff y = 'not' x;

definition let L be non empty RelStr,
a,b be Element of L;
func a \ b -> Element of L equals
:: YELLOW_5:def 1
a "/\" 'not' b;
end;

definition let L be non empty RelStr,
a, b be Element of L;
func a \+\ b -> Element of L equals
:: YELLOW_5:def 2
(a \ b) "\/" (b \ a);
end;

definition let L be antisymmetric with_infima with_suprema RelStr,
a, b be Element of L;
redefine func a \+\ b;
commutativity;
end;

definition let L be non empty RelStr,
a, b be Element of L;
pred a meets b means
:: YELLOW_5:def 3
a "/\" b <> Bottom L;
antonym a misses b;
end;

definition let L be with_infima antisymmetric RelStr,
a, b be Element of L;
redefine pred a meets b;
symmetry;
antonym a misses b;
end;

theorem :: YELLOW_5:12
for L be antisymmetric transitive with_infima with_suprema RelStr
for a,b,c be Element of L holds
a <= c implies a \ b <= c;

theorem :: YELLOW_5:13
for L be antisymmetric transitive with_infima with_suprema RelStr
for a,b,c be Element of L holds
a <= b implies a \ c <= b \ c;

theorem :: YELLOW_5:14
for L be antisymmetric transitive with_infima with_suprema RelStr
for a,b be Element of L holds
a \ b <= a;

theorem :: YELLOW_5:15
for L be antisymmetric transitive with_infima with_suprema RelStr
for a,b be Element of L holds
a \ b <= a \+\ b;

theorem :: YELLOW_5:16
for L be LATTICE
for a,b,c be Element of L holds
a \ b <= c & b \ a <= c implies a \+\ b <= c;

theorem :: YELLOW_5:17
for L be LATTICE
for a be Element of L holds
a meets a iff a <> Bottom L;

theorem :: YELLOW_5:18
for L be antisymmetric transitive with_infima with_suprema RelStr
for a,b,c be Element of L holds
a "/\" (b \ c) = (a "/\" b) \ c;

theorem :: YELLOW_5:19
for L be antisymmetric transitive with_infima RelStr st
L is distributive
for a,b,c be Element of L holds
(a "/\" b) "\/" (a "/\" c) = a implies a <= b "\/" c;

theorem :: YELLOW_5:20
for L be LATTICE st L is distributive
for a,b,c be Element of L holds
a"\/"(b"/\"c) = (a"\/"b) "/\" (a"\/"c);

theorem :: YELLOW_5:21
for L be LATTICE st L is distributive
for a,b,c be Element of L holds
(a "\/" b) \ c = (a \ c) "\/" (b \ c);

:: Lower-bound in Relation Structure
begin

theorem :: YELLOW_5:22
for L be lower-bounded non empty antisymmetric RelStr
for a be Element of L holds
a <= Bottom L implies a = Bottom L;

theorem :: YELLOW_5:23
for L be lower-bounded Semilattice
for a,b,c be Element of L holds
a <= b & a <= c & b"/\"c = Bottom L implies a = Bottom L;

theorem :: YELLOW_5:24
for L be lower-bounded antisymmetric with_suprema RelStr
for a,b be Element of L holds
a"\/"b = Bottom L implies a = Bottom L & b = Bottom L;

theorem :: YELLOW_5:25
for L be lower-bounded antisymmetric transitive with_infima RelStr
for a,b,c be Element of L holds
a <= b & b"/\"c = Bottom L implies a"/\"c = Bottom L;

theorem :: YELLOW_5:26
for L be lower-bounded Semilattice
for a be Element of L holds
Bottom L \ a = Bottom L;

theorem :: YELLOW_5:27
for L be lower-bounded antisymmetric transitive with_infima RelStr
for a,b,c be Element of L holds
a meets b & b <= c implies a meets c;

theorem :: YELLOW_5:28
for L be lower-bounded with_infima antisymmetric RelStr
for a be Element of L holds
a"/\"Bottom L = Bottom L;

theorem :: YELLOW_5:29
for L be lower-bounded antisymmetric transitive
with_infima with_suprema RelStr
for a,b,c be Element of L holds
a meets b"/\"c implies a meets b;

theorem :: YELLOW_5:30
for L be lower-bounded antisymmetric transitive
with_infima with_suprema RelStr
for a,b,c be Element of L holds
a meets b\c implies a meets b;

theorem :: YELLOW_5:31
for L be lower-bounded antisymmetric transitive with_infima RelStr
for a be Element of L holds
a misses Bottom L;

theorem :: YELLOW_5:32
for L be lower-bounded antisymmetric transitive with_infima RelStr
for a,b,c be Element of L holds
a misses c & b <= c implies a misses b;

theorem :: YELLOW_5:33
for L be lower-bounded antisymmetric transitive with_infima RelStr
for a,b,c be Element of L holds
a misses b or a misses c implies a misses b"/\"c;

theorem :: YELLOW_5:34
for L be lower-bounded LATTICE
for a,b,c be Element of L holds
a <= b & a <= c & b misses c implies a = Bottom L;

theorem :: YELLOW_5:35
for L be lower-bounded antisymmetric transitive with_infima RelStr
for a,b,c be Element of L holds
a misses b implies (a"/\"c) misses (b"/\"c);

:: Boolean Lattice
begin

reserve L for Boolean (non empty RelStr);
reserve a,b,c,d for Element of L;

theorem :: YELLOW_5:36
(a"/\"b) "\/" (b"/\"c) "\/" (c"/\"a) = (a"\/"b) "/\" (b"\/"c) "/\" (c"\/"a);

theorem :: YELLOW_5:37
a"/\"'not' a = Bottom L & a"\/"'not' a = Top L;

theorem :: YELLOW_5:38
a \ b <= c implies a <= b"\/"c;

theorem :: YELLOW_5:39
'not' (a"\/"b) = 'not' a"/\" 'not' b & 'not' (a"/\"b) = 'not' a"\/" 'not' b;

theorem :: YELLOW_5:40
a <= b implies 'not' b <= 'not' a;

theorem :: YELLOW_5:41
a <= b implies c\b <= c\a;

theorem :: YELLOW_5:42
a <= b & c <= d implies a\d <= b\c;

theorem :: YELLOW_5:43
a <= b"\/"c implies a\b <= c & a\c <= b;

theorem :: YELLOW_5:44
'not' a <= 'not' (a"/\"b) & 'not' b <= 'not' (a"/\"b);

theorem :: YELLOW_5:45
'not' (a"\/"b) <= 'not' a & 'not' (a"\/"b) <= 'not' b;

theorem :: YELLOW_5:46
a <= b\a implies a = Bottom L;

theorem :: YELLOW_5:47
a <= b implies b = a "\/" (b\a);

theorem :: YELLOW_5:48
a\b = Bottom L iff a <= b;

theorem :: YELLOW_5:49
(a <= b"\/"c & a"/\"c = Bottom L) implies a <= b;

theorem :: YELLOW_5:50
a"\/"b = (a\b)"\/"b;

theorem :: YELLOW_5:51
a\(a"\/"b) = Bottom L;

theorem :: YELLOW_5:52
a\a"/\"b = a\b;

theorem :: YELLOW_5:53
(a\b)"/\"b = Bottom L;

theorem :: YELLOW_5:54
a"\/"(b\a) = a"\/"b;

theorem :: YELLOW_5:55
(a"/\"b)"\/"(a\b) = a;

theorem :: YELLOW_5:56
a\(b\c)= (a\b)"\/"(a"/\"c);

theorem :: YELLOW_5:57
a\(a\b) = a"/\"b;

theorem :: YELLOW_5:58
(a"\/"b)\b = a\b;

theorem :: YELLOW_5:59
a"/\"b = Bottom L iff a\b = a;

theorem :: YELLOW_5:60
a\(b"\/"c) = (a\b)"/\"(a\c);

theorem :: YELLOW_5:61
a\(b"/\"c) = (a\b)"\/"(a\c);

theorem :: YELLOW_5:62
a"/\"(b\c) = a"/\"b \ a"/\"c;

theorem :: YELLOW_5:63
(a"\/"b)\(a"/\"b) = (a\b)"\/"(b\a);

theorem :: YELLOW_5:64
(a\b)\c = a\(b"\/"c);

theorem :: YELLOW_5:65
'not' (Bottom L) = Top L;

theorem :: YELLOW_5:66
'not' (Top L) = Bottom L;

theorem :: YELLOW_5:67
a\a = Bottom L;

theorem :: YELLOW_5:68
a \ Bottom L = a;

theorem :: YELLOW_5:69
'not' (a\b) = 'not' a"\/"b;

theorem :: YELLOW_5:70
a"/\"b misses a\b;

theorem :: YELLOW_5:71
(a\b) misses b;

theorem :: YELLOW_5:72
a misses b implies (a"\/"b)\b = a;

```