The abstract of the Mizar article:

Complete Lattices

by

Grzegorz Bancerek

Received May 13, 1992

MML identifier: LATTICE3

[ Mizar article, MML identifier index ]

environ

 vocabulary LATTICES, FUNCT_1, BOOLE, BINOP_1, SUBSET_1, FILTER_1, ORDERS_1,
      RELAT_1, RELAT_2, BHSP_3, FILTER_0, TARSKI, ZF_LANG, LATTICE3, PARTFUN1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, STRUCT_0, FUNCT_1,
      FUNCT_2, BINOP_1, LATTICES, FILTER_0, LATTICE2, FILTER_1, RELAT_1,
      RELAT_2, RELSET_1, PARTFUN1, ORDERS_1;
 constructors DOMAIN_1, BINOP_1, LATTICE2, FILTER_1, RELAT_2, ORDERS_1,
      ORDERS_2, MEMBERED, PARTFUN1, XBOOLE_0;
 clusters LATTICE2, ORDERS_1, RELSET_1, STRUCT_0, RLSUB_2, SUBSET_1, LATTICES,
      MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

definition let X be set;
 func BooleLatt X -> strict LattStr means
:: LATTICE3:def 1
  the carrier of it = bool X &
  for Y,Z being Element of bool X holds
   (the L_join of it).(Y,Z) = Y \/ Z & (the L_meet of it).(Y,Z) = Y /\ Z;
end;

reserve X for set,
        x,y,z for Element of BooleLatt X, s for set;

definition let X be set;
 cluster BooleLatt X -> non empty;
end;

theorem :: LATTICE3:1
 x "\/" y = x \/ y & x "/\" y = x /\ y;

theorem :: LATTICE3:2
 x [= y iff x c= y;

definition let X;
 cluster BooleLatt X -> Lattice-like;
end;

reserve y for Element of BooleLatt X;

theorem :: LATTICE3:3
 BooleLatt X is lower-bounded & Bottom BooleLatt X = {};

theorem :: LATTICE3:4
 BooleLatt X is upper-bounded & Top BooleLatt X = X;

definition let X;
 cluster BooleLatt X -> Boolean Lattice-like;
end;

theorem :: LATTICE3:5
   for x being Element of BooleLatt X holds x` = X \ x;

begin :: Correspondence Between Lattices and Posets

definition let L be Lattice;
 redefine func LattRel L -> Order of the carrier of L;
end;

definition let L be Lattice;
 func LattPOSet L -> strict Poset equals
:: LATTICE3:def 2
    RelStr(#the carrier of L, LattRel L#);
end;

definition let L be Lattice;
  cluster LattPOSet L -> non empty;
end;

theorem :: LATTICE3:6
 for L1,L2 being Lattice st LattPOSet L1 = LattPOSet L2 holds
   the LattStr of L1 = the LattStr of L2;

definition let L be Lattice, p be Element of L;
 func p% -> Element of LattPOSet L equals
:: LATTICE3:def 3
   p;
end;

definition let L be Lattice, p be Element of LattPOSet L;
 func %p -> Element of L equals
:: LATTICE3:def 4
   p;
end;

reserve L for Lattice, p,q for Element of L;

theorem :: LATTICE3:7
 p [= q iff p% <= q%;

 definition let X be set, O be Order of X;
  redefine func O~ -> Order of X;
 end;

definition let A be RelStr;
 func A~ -> strict RelStr equals
:: LATTICE3:def 5

   RelStr(#the carrier of A, (the InternalRel of A)~#);
end;

definition let A be Poset;
 cluster A~ -> reflexive transitive antisymmetric;
end;

definition let A be non empty RelStr;
 cluster A~ -> non empty;
end;

reserve A for RelStr, a,b,c for Element of A;

theorem :: LATTICE3:8
   A~~ = the RelStr of A;

definition let A be RelStr, a be Element of A;
 func a~ -> Element of A~ equals
:: LATTICE3:def 6
    a;
end;

definition let A be RelStr, a be Element of A~;
 func ~a -> Element of A equals
:: LATTICE3:def 7
    a;
end;

theorem :: LATTICE3:9
 a <= b iff b~ <= a~;

definition let A be RelStr, X be set, a be Element of A;
 pred a is_<=_than X means
:: LATTICE3:def 8
for b being Element of A st b in X
   holds a <= b;
  synonym X is_>=_than a;
 pred X is_<=_than a means
:: LATTICE3:def 9

  for b being Element of A st b in X holds b <= a;
  synonym a is_>=_than X;
end;

definition let IT be RelStr;
 attr IT is with_suprema means
:: LATTICE3:def 10

  for x,y being Element of IT
   ex z being Element of IT st x <= z & y <= z &
    for z' being Element of IT st x <= z' & y <= z' holds z <= z';
 attr IT is with_infima means
:: LATTICE3:def 11

  for x,y being Element of IT
   ex z being Element of IT st z <= x & z <= y &
    for z' being Element of IT st z' <= x & z' <= y holds z' <= z;
end;

definition
 cluster with_suprema -> non empty RelStr;
 cluster with_infima -> non empty RelStr;
end;

theorem :: LATTICE3:10
   A is with_suprema iff A~ is with_infima;

theorem :: LATTICE3:11
   for L being Lattice holds LattPOSet L is with_suprema with_infima;

definition let IT be RelStr;
 attr IT is complete means
:: LATTICE3:def 12

  for X being set ex a being Element of IT st X is_<=_than a &
   for b being Element of IT st X is_<=_than b holds a <= b;
end;

definition
 cluster strict complete non empty Poset;
end;

reserve A for non empty RelStr, a,b,c,c' for Element of A;

theorem :: LATTICE3:12
 A is complete implies A is with_suprema with_infima;

definition
 cluster complete with_suprema with_infima strict non empty Poset;
end;

definition let A be RelStr such that
 A is antisymmetric;
 let a,b be Element of A such that
 ex x being Element of A st a <= x & b <= x &
   for c being Element of A st a <= c & b <= c holds x <= c;
 func a"\/"b -> Element of A means
:: LATTICE3:def 13
   a <= it & b <= it &
   for c being Element of A st a <= c & b <= c holds it <= c;
end;

definition let A be RelStr such that
 A is antisymmetric;
 let a,b be Element of A such that
 ex x being Element of A st a >= x & b >= x &
   for c being Element of A st a >= c & b >= c holds x >= c;
 func a"/\"b -> Element of A means
:: LATTICE3:def 14
   it <= a & it <= b &
   for c being Element of A st c <= a & c <= b holds c <= it;
end;

reserve V for with_suprema antisymmetric RelStr,
 u1,u2,u3,u4 for Element of V;
reserve N for with_infima antisymmetric RelStr,
 n1,n2,n3,n4 for Element of N;
reserve K for with_suprema with_infima reflexive antisymmetric RelStr,
  k1,k2,k3 for Element of K;

theorem :: LATTICE3:13
 u1 "\/" u2 = u2 "\/" u1;

theorem :: LATTICE3:14
 V is transitive implies (u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3);

theorem :: LATTICE3:15
 n1 "/\" n2 = n2 "/\" n1;

theorem :: LATTICE3:16
 N is transitive implies (n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3);

definition let L be with_infima antisymmetric RelStr,
               x, y be Element of L;
 redefine func x "/\" y;
 commutativity;
end;

definition let L be with_suprema antisymmetric RelStr,
               x, y be Element of L;
 redefine func x "\/" y;
commutativity;
end;

theorem :: LATTICE3:17
 (k1 "/\" k2) "\/" k2 = k2;

theorem :: LATTICE3:18
 k1 "/\" (k1 "\/" k2) = k1;

theorem :: LATTICE3:19
 for A being with_suprema with_infima Poset
   ex L being strict Lattice st the RelStr of A = LattPOSet L;

definition let A be RelStr such that
  A is with_suprema with_infima Poset;
 func latt A -> strict Lattice means
:: LATTICE3:def 15

  the RelStr of A = LattPOSet it;
end;

theorem :: LATTICE3:20
   (LattRel L)~ = LattRel (L.:) & (LattPOSet L)~ = LattPOSet (L.:);

begin :: Complete Lattice

definition
 let L be non empty LattStr, p be Element of L, X be set;
 pred p is_less_than X means
:: LATTICE3:def 16
   for q being Element of L st q in X holds p [= q;
  synonym X is_great_than p;

 pred X is_less_than p means
:: LATTICE3:def 17
   for q being Element of L st q in X holds q [= p;
  synonym p is_great_than X;
end;

theorem :: LATTICE3:21
   for L being Lattice, p,q,r being Element of L holds
   p is_less_than {q,r} iff p [= q"/\"r;

theorem :: LATTICE3:22
   for L being Lattice, p,q,r being Element of L holds
  p is_great_than {q,r} iff q"\/"r [= p;

definition let IT be non empty LattStr;
 attr IT is complete means
:: LATTICE3:def 18
  for X being set ex p being Element of IT st X is_less_than p &
    for r being Element of IT st X is_less_than r holds p [= r;

 attr IT is \/-distributive means
:: LATTICE3:def 19
  for X for a,b,c being Element of IT st X is_less_than a &
   (for d being Element of IT st X is_less_than d holds a [= d)
    & {b"/\"a' where a' is Element of IT: a' in
 X} is_less_than c &
   for d being Element of IT st
    {b"/\"a' where a' is Element of IT: a' in X} is_less_than d
    holds c [= d
   holds b"/\"a [= c;

 attr IT is /\-distributive means
:: LATTICE3:def 20
    for X for a,b,c being Element of IT st X is_great_than a &
   (for d being Element of IT st X is_great_than d holds d [= a)
   & {b"\/"a' where a' is Element of IT: a' in
 X} is_great_than c &
   for d being Element of IT st
    {b"\/"a' where a' is Element of IT: a' in X} is_great_than d
    holds d [= c
   holds c [= b"\/"a;
end;

theorem :: LATTICE3:23
   for B being B_Lattice, a being Element of B holds
   X is_less_than a iff {b` where b is Element of B: b in X}
    is_great_than a`;

theorem :: LATTICE3:24
 for B being B_Lattice, a being Element of B holds
   X is_great_than a iff {b` where b is Element of B: b in X}
    is_less_than a`;

theorem :: LATTICE3:25
 BooleLatt X is complete;

theorem :: LATTICE3:26
 BooleLatt X is \/-distributive;

theorem :: LATTICE3:27
 BooleLatt X is /\-distributive;

definition
 cluster complete \/-distributive /\-distributive strict Lattice;
end;

reserve p',q' for Element of LattPOSet L;

theorem :: LATTICE3:28
 p is_less_than X iff p% is_<=_than X;

theorem :: LATTICE3:29
   p' is_<=_than X iff %p' is_less_than X;

theorem :: LATTICE3:30
 X is_less_than p iff X is_<=_than p%;

theorem :: LATTICE3:31
 X is_<=_than p' iff X is_less_than %p';

 definition let A be complete (non empty Poset);
  cluster latt A -> complete;
 end;

definition let L be non empty LattStr such that
 L is complete Lattice;
 let X be set;
 func "\/"(X,L) -> Element of L means
:: LATTICE3:def 21

  X is_less_than it &
   for r being Element of L st X is_less_than r holds it [= r;
end;

definition let L be non empty LattStr, X be set;
 func "/\"(X,L) -> Element of L equals
:: LATTICE3:def 22
   "\/"({p where p is Element of L: p is_less_than X},L);
end;

definition let L be non empty LattStr, X be Subset of L;
 redefine func "\/"(X,L); synonym "\/" X; func "/\"(X,L); synonym "/\" X;
end;

reserve C for complete Lattice,
        a,a',b,b',c,d for Element of C, X,Y for set;

theorem :: LATTICE3:32
 "\/"({a"/\"b: b in X}, C) [= a"/\""\/"(X,C);

theorem :: LATTICE3:33
 C is \/-distributive iff for X, a holds a"/\""\/"(X,C) [= "\/"({a"/\"
b: b in X}, C);

theorem :: LATTICE3:34
 a = "/\"(X,C) iff a is_less_than X & for b st b is_less_than X holds b [= a;

theorem :: LATTICE3:35
 a"\/""/\"(X,C) [= "/\"({a"\/"b: b in X}, C);

theorem :: LATTICE3:36
 C is /\-distributive iff for X, a holds "/\"({a"\/"b: b in X}, C) [= a"\/""/\"
(X,C);

theorem :: LATTICE3:37
   "\/"(X,C) = "/\"({a: a is_great_than X}, C);

theorem :: LATTICE3:38
 a in X implies a [= "\/"(X,C) & "/\"(X,C) [= a;

canceled;

theorem :: LATTICE3:40
 a is_less_than X implies a [= "/\"(X,C);

theorem :: LATTICE3:41
 a in X & X is_less_than a implies "\/"(X,C) = a;

theorem :: LATTICE3:42
 a in X & a is_less_than X implies "/\"(X,C) = a;

theorem :: LATTICE3:43
   "\/"{a} = a & "/\"{a} = a;

theorem :: LATTICE3:44
    a"\/"b = "\/"{a,b} & a"/\"b = "/\"{a,b};

theorem :: LATTICE3:45
   a = "\/"({b: b [= a}, C) & a = "/\"({c: a [= c}, C);

theorem :: LATTICE3:46
 X c= Y implies "\/"(X,C) [= "\/"(Y,C) & "/\"(Y,C) [= "/\"(X,C);

theorem :: LATTICE3:47
 "\/"(X,C) = "\/"({a: ex b st a [= b & b in X}, C) &
   "/\"(X,C) = "/\"({b: ex a st a [= b & a in X}, C);

theorem :: LATTICE3:48
    (for a st a in X ex b st a [= b & b in Y) implies "\/"(X,C) [= "\/"(Y,C);

theorem :: LATTICE3:49
   X c= bool the carrier of C implies
   "\/"(union X, C) = "\/"({"\/"
Y where Y is Subset of C: Y in X}, C);

theorem :: LATTICE3:50
   C is 0_Lattice & Bottom C = "\/"({},C);

theorem :: LATTICE3:51
   C is 1_Lattice & Top C = "\/"(the carrier of C, C);

theorem :: LATTICE3:52
 C is I_Lattice implies a => b = "\/"({c: a"/\"c [= b}, C);

theorem :: LATTICE3:53
   C is I_Lattice implies C is \/-distributive;

theorem :: LATTICE3:54
   for D being complete \/-distributive Lattice,
     a being Element of D holds
  a "/\" "\/"(X,D) = "\/"({a"/\"
b1 where b1 is Element of D: b1 in
 X}, D) &
  "\/"(X,D) "/\" a = "\/"({b2"/\"
a where b2 is Element of D: b2 in
 X}, D);

theorem :: LATTICE3:55
   for D being complete /\-distributive Lattice,
     a being Element of D holds
  a "\/" "/\"(X,D)
    = "/\"({a"\/"b1 where b1 is Element of D: b1 in X}, D) &
  "/\"(X,D) "\/" a = "/\"({b2"\/"
a where b2 is Element of D: b2 in
 X}, D);

scheme SingleFraenkel{A()->set, B()->non empty set, P[set]}:
  {A() where a is Element of B(): P[a]} = {A()}
  provided
 ex a being Element of B() st P[a];

scheme FuncFraenkel{B()->non empty set, C()->non empty set,
        A(set)->Element of C(),f()->Function, P[set]}:
  f().:{A(x) where x is Element of B(): P[x]} =
   {f().A(x) where x is Element of B(): P[x]}
  provided
  C() c= dom f();

theorem :: LATTICE3:56
   for D being non empty set, f being Function of bool D, D st
   (for a being Element of D holds f.{a} = a) &
   for X being Subset of bool D holds f.(f.:X) = f.(union X)
  ex L being complete strict Lattice st the carrier of L = D &
   for X being Subset of L holds "\/" X = f.X;