The abstract of the Mizar article:

Definitions and Properties of the Join and Meet of Subsets

by

Artur Kornilowicz

Received September 25, 1996

MML identifier: YELLOW_4

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, YELLOW_0, LATTICES, LATTICE3, SETFAM_1, RELAT_2, BOOLE,
      WAYBEL_0, QUANTAL1, ORDINAL2, BHSP_3, YELLOW_1, TARSKI, FUNCT_5;
 notation TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, LATTICE3, YELLOW_0, STRUCT_0,
      ORDERS_1, YELLOW_1, WAYBEL_0, YELLOW_3;
 constructors YELLOW_2, YELLOW_3, LATTICE3, MEMBERED, PRE_TOPC;
 clusters STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_2, SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

theorem :: YELLOW_4:1
for L being RelStr, X being set, a being Element of L
 st a in X & ex_sup_of X,L holds a <= "\/"(X,L);

theorem :: YELLOW_4:2
for L being RelStr, X being set, a being Element of L
 st a in X & ex_inf_of X,L holds "/\"(X,L) <= a;

definition let L be RelStr,
               A, B be Subset of L;
 pred A is_finer_than B means
:: YELLOW_4:def 1
  for a being Element of L st a in A ex b being Element of L st b in
 B & a <= b;
 pred B is_coarser_than A means
:: YELLOW_4:def 2
  for b being Element of L st b in B ex a being Element of L st a in
 A & a <= b;
end;

definition let L be non empty reflexive RelStr,
               A, B be Subset of L;
 redefine pred A is_finer_than B;
reflexivity;
 redefine pred B is_coarser_than A;
reflexivity;
end;

theorem :: YELLOW_4:3
  for L being RelStr, B being Subset of L holds {}L is_finer_than B;

theorem :: YELLOW_4:4
  for L being transitive RelStr, A, B, C being Subset of L
 st A is_finer_than B & B is_finer_than C holds A is_finer_than C;

theorem :: YELLOW_4:5
  for L being RelStr, A, B being Subset of L st B is_finer_than A & A is lower
 holds B c= A;

theorem :: YELLOW_4:6
  for L being RelStr, A being Subset of L holds {}L is_coarser_than A;

theorem :: YELLOW_4:7
  for L being transitive RelStr, A, B, C being Subset of L
 st C is_coarser_than B & B is_coarser_than A holds C is_coarser_than A;

theorem :: YELLOW_4:8
  for L being RelStr, A, B being Subset of L st A is_coarser_than B & B is
upper
 holds A c= B;


begin :: The Join of Subsets

definition let L be non empty RelStr,
               D1, D2 be Subset of L;
 func D1 "\/" D2 -> Subset of L equals
:: YELLOW_4:def 3
   { x "\/" y where x, y is Element of L : x in D1 & y in D2 };
end;

definition let L be with_suprema antisymmetric RelStr,
               D1, D2 be Subset of L;
 redefine func D1 "\/" D2;
commutativity;
end;

theorem :: YELLOW_4:9
  for L being non empty RelStr, X being Subset of L holds X "\/" {}L = {};

theorem :: YELLOW_4:10
for L being non empty RelStr, X, Y being Subset of L, x, y being Element of L
 st x in X & y in Y holds x "\/" y in X "\/" Y;

theorem :: YELLOW_4:11
  for L being antisymmetric with_suprema RelStr
 for A being Subset of L, B being non empty Subset of L
  holds A is_finer_than A "\/" B;

theorem :: YELLOW_4:12
  for L being antisymmetric with_suprema RelStr, A, B being Subset of L
 holds A "\/" B is_coarser_than A;

theorem :: YELLOW_4:13
  for L being antisymmetric reflexive with_suprema RelStr
 for A being Subset of L holds A c= A "\/" A;

theorem :: YELLOW_4:14
  for L being with_suprema antisymmetric transitive RelStr
 for D1, D2, D3 being Subset of L holds (D1 "\/" D2) "\/" D3 = D1 "\/" (D2 "\/"
 D3);

definition let L be non empty RelStr,
               D1, D2 be non empty Subset of L;
 cluster D1 "\/" D2 -> non empty;
end;

definition let L be with_suprema transitive antisymmetric RelStr,
               D1, D2 be directed Subset of L;
 cluster D1 "\/" D2 -> directed;
end;

definition let L be with_suprema transitive antisymmetric RelStr,
               D1, D2 be filtered Subset of L;
 cluster D1 "\/" D2 -> filtered;
end;

definition let L be with_suprema Poset,
               D1, D2 be upper Subset of L;
 cluster D1 "\/" D2 -> upper;
end;

theorem :: YELLOW_4:15
for L being non empty RelStr, Y being Subset of L, x being Element of L
 holds {x} "\/" Y = {x "\/" y where y is Element of L: y in Y};

theorem :: YELLOW_4:16
  for L being non empty RelStr, A, B, C being Subset of L
 holds A "\/" (B \/ C) = (A "\/" B) \/ (A "\/" C);

theorem :: YELLOW_4:17
  for L being antisymmetric reflexive with_suprema RelStr
 for A, B, C being Subset of L holds A \/ (B "\/" C) c= (A \/ B) "\/" (A \/ C);

theorem :: YELLOW_4:18
  for L being antisymmetric with_suprema RelStr, A being upper Subset of L
 for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C);

theorem :: YELLOW_4:19
  for L being non empty RelStr, x, y being Element of L
  holds {x} "\/" {y} = {x "\/" y};

theorem :: YELLOW_4:20
  for L being non empty RelStr, x, y, z being Element of L
  holds {x} "\/" {y,z} = {x "\/" y, x "\/" z};

theorem :: YELLOW_4:21
  for L being non empty RelStr, X1, X2, Y1, Y2 being Subset of L st
 X1 c= Y1 & X2 c= Y2 holds X1 "\/" X2 c= Y1 "\/" Y2;

theorem :: YELLOW_4:22
  for L being with_suprema reflexive antisymmetric RelStr
 for D being Subset of L, x being Element of L st x is_<=_than D
  holds {x} "\/" D = D;

theorem :: YELLOW_4:23
  for L being with_suprema antisymmetric RelStr
 for D being Subset of L, x being Element of L
  holds x is_<=_than {x} "\/" D;

theorem :: YELLOW_4:24
  for L being with_suprema Poset, X being Subset of L, x being Element of L
 st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds x "\/" inf X <= inf ({x} "\/"
 X);

theorem :: YELLOW_4:25
for L being complete transitive antisymmetric (non empty RelStr)
 for A being Subset of L, B being non empty Subset of L
  holds A is_<=_than sup (A "\/" B);

theorem :: YELLOW_4:26
  for L being with_suprema transitive antisymmetric RelStr
 for a, b being Element of L, A, B being Subset of L
  st a is_<=_than A & b is_<=_than B holds a "\/" b is_<=_than A "\/" B;

theorem :: YELLOW_4:27
for L being with_suprema transitive antisymmetric RelStr
 for a, b being Element of L, A, B being Subset of L
  st a is_>=_than A & b is_>=_than B holds a "\/" b is_>=_than A "\/" B;

theorem :: YELLOW_4:28
  for L being complete (non empty Poset)
 for A, B being non empty Subset of L holds sup (A "\/" B) = sup A "\/" sup B;

theorem :: YELLOW_4:29
for L being with_suprema antisymmetric RelStr
 for X being Subset of L, Y being non empty Subset of L holds
  X c= downarrow (X "\/" Y);

theorem :: YELLOW_4:30
  for L being with_suprema Poset
 for x, y being Element of InclPoset Ids L
  for X, Y being Subset of L st x = X & y = Y
 holds x "\/" y = downarrow (X "\/" Y);

theorem :: YELLOW_4:31
  for L being non empty RelStr, D being Subset of [:L,L:] holds
 union {X where X is Subset of L: ex x being Element of L st X = {x} "\/"
 proj2 D
  & x in proj1 D} = proj1 D "\/" proj2 D;

theorem :: YELLOW_4:32
for L being transitive antisymmetric with_suprema RelStr
 for D1, D2 being Subset of L holds
  downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2);

theorem :: YELLOW_4:33
  for L being with_suprema Poset, D1, D2 being Subset of L holds
 downarrow ((downarrow D1) "\/" (downarrow D2)) = downarrow (D1 "\/" D2);

theorem :: YELLOW_4:34
for L being transitive antisymmetric with_suprema RelStr
 for D1, D2 being Subset of L holds
  uparrow ((uparrow D1) "\/" (uparrow D2)) c= uparrow (D1 "\/" D2);

theorem :: YELLOW_4:35
  for L being with_suprema Poset, D1, D2 being Subset of L holds
 uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2);


begin :: The Meet of Subsets

definition let L be non empty RelStr,
               D1, D2 be Subset of L;
 func D1 "/\" D2 -> Subset of L equals
:: YELLOW_4:def 4
   { x "/\" y where x, y is Element of L : x in D1 & y in D2 };
end;

definition let L be with_infima antisymmetric RelStr,
               D1, D2 be Subset of L;
 redefine func D1 "/\" D2;
commutativity;
end;

theorem :: YELLOW_4:36
  for L being non empty RelStr, X being Subset of L holds X "/\" {}L = {};

theorem :: YELLOW_4:37
for L being non empty RelStr, X, Y being Subset of L, x, y being Element of L
 st x in X & y in Y holds x "/\" y in X "/\" Y;

theorem :: YELLOW_4:38
  for L being antisymmetric with_infima RelStr
 for A being Subset of L, B being non empty Subset of L
  holds A is_coarser_than A "/\" B;

theorem :: YELLOW_4:39
  for L being antisymmetric with_infima RelStr
 for A, B being Subset of L holds A "/\" B is_finer_than A;

theorem :: YELLOW_4:40
  for L being antisymmetric reflexive with_infima RelStr
 for A being Subset of L holds A c= A "/\" A;

theorem :: YELLOW_4:41
  for L being with_infima antisymmetric transitive RelStr
 for D1, D2, D3 being Subset of L holds (D1 "/\" D2) "/\" D3 = D1 "/\" (D2 "/\"
 D3);

definition let L be non empty RelStr,
               D1, D2 be non empty Subset of L;
 cluster D1 "/\" D2 -> non empty;
end;

definition let L be with_infima transitive antisymmetric RelStr,
               D1, D2 be directed Subset of L;
 cluster D1 "/\" D2 -> directed;
end;

definition let L be with_infima transitive antisymmetric RelStr,
               D1, D2 be filtered Subset of L;
 cluster D1 "/\" D2 -> filtered;
end;

definition let L be Semilattice,
               D1, D2 be lower Subset of L;
 cluster D1 "/\" D2 -> lower;
end;

theorem :: YELLOW_4:42
for L being non empty RelStr, Y being Subset of L, x being Element of L
 holds {x} "/\" Y = {x "/\" y where y is Element of L: y in Y};

theorem :: YELLOW_4:43
  for L being non empty RelStr, A, B, C being Subset of L
 holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C);

theorem :: YELLOW_4:44
  for L being antisymmetric reflexive with_infima RelStr
 for A, B, C being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C);

theorem :: YELLOW_4:45
  for L being antisymmetric with_infima RelStr, A being lower Subset of L
 for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C);

theorem :: YELLOW_4:46
  for L being non empty RelStr, x, y being Element of L
  holds {x} "/\" {y} = {x "/\" y};

theorem :: YELLOW_4:47
  for L being non empty RelStr, x, y, z being Element of L
  holds {x} "/\" {y,z} = {x "/\" y, x "/\" z};

theorem :: YELLOW_4:48
  for L being non empty RelStr, X1, X2, Y1, Y2 being Subset of L st
 X1 c= Y1 & X2 c= Y2 holds X1 "/\" X2 c= Y1 "/\" Y2;

theorem :: YELLOW_4:49
for L being antisymmetric reflexive with_infima RelStr
 for A, B being Subset of L holds A /\ B c= A "/\" B;

theorem :: YELLOW_4:50
for L being antisymmetric reflexive with_infima RelStr
 for A, B being lower Subset of L holds A "/\" B = A /\ B;

theorem :: YELLOW_4:51
  for L being with_infima reflexive antisymmetric RelStr
 for D being Subset of L, x being Element of L st x is_>=_than D
  holds {x} "/\" D = D;

theorem :: YELLOW_4:52
  for L being with_infima antisymmetric RelStr
 for D being Subset of L, x being Element of L
  holds {x} "/\" D is_<=_than x;

theorem :: YELLOW_4:53
  for L being Semilattice, X being Subset of L, x being Element of L st
 ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds sup ({x} "/\" X) <= x "/\" sup X;

theorem :: YELLOW_4:54
for L being complete transitive antisymmetric (non empty RelStr)
 for A being Subset of L, B being non empty Subset of L
  holds A is_>=_than inf (A "/\" B);

theorem :: YELLOW_4:55
for L being with_infima transitive antisymmetric RelStr
 for a, b being Element of L, A, B being Subset of L
  st a is_<=_than A & b is_<=_than B holds a "/\" b is_<=_than A "/\" B;

theorem :: YELLOW_4:56
  for L being with_infima transitive antisymmetric RelStr
 for a, b being Element of L, A, B being Subset of L
  st a is_>=_than A & b is_>=_than B holds a "/\" b is_>=_than A "/\" B;

theorem :: YELLOW_4:57
  for L being complete (non empty Poset)
 for A, B being non empty Subset of L holds inf (A "/\" B) = inf A "/\" inf B;

theorem :: YELLOW_4:58
  for L being Semilattice, x, y being Element of InclPoset Ids L
 for x1, y1 being Subset of L st x = x1 & y = y1 holds x "/\" y = x1 "/\" y1;

theorem :: YELLOW_4:59
  for L being with_infima antisymmetric RelStr
 for X being Subset of L, Y being non empty Subset of L holds
  X c= uparrow (X "/\" Y);

theorem :: YELLOW_4:60
  for L being non empty RelStr, D being Subset of [:L,L:] holds
 union {X where X is Subset of L: ex x being Element of L st X = {x} "/\"
 proj2 D
  & x in proj1 D} = proj1 D "/\" proj2 D;

theorem :: YELLOW_4:61
for L being transitive antisymmetric with_infima RelStr
 for D1, D2 being Subset of L holds
  downarrow ((downarrow D1) "/\" (downarrow D2)) c= downarrow (D1 "/\" D2);

theorem :: YELLOW_4:62
  for L being Semilattice, D1, D2 being Subset of L holds
 downarrow ((downarrow D1) "/\" (downarrow D2)) = downarrow (D1 "/\" D2);

theorem :: YELLOW_4:63
for L being transitive antisymmetric with_infima RelStr
 for D1, D2 being Subset of L holds
  uparrow ((uparrow D1) "/\" (uparrow D2)) c= uparrow (D1 "/\" D2);

theorem :: YELLOW_4:64
  for L being Semilattice, D1, D2 being Subset of L holds
 uparrow ((uparrow D1) "/\" (uparrow D2)) = uparrow (D1 "/\" D2);