The abstract of the Mizar article:

Miscellaneous Facts about Relation Structure

by

Agnieszka Julia Marasik

Received November 8, 1996

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;