The abstract of the Mizar article:

Finite Join and Finite Meet, and Dual Lattices

by

Andrzej Trybulec

Received August 10, 1990

MML identifier: LATTICE2

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCT_4, FINSUB_1, BINOP_1, LATTICES,
      SETWISEO, FUNCOP_1, FILTER_0, FINSET_1, LATTICE2;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4,
      PARTFUN1, FUNCOP_1, BINOP_1, STRUCT_0, LATTICES, FINSET_1, FINSUB_1,
      GROUP_1, SETWISEO, FILTER_0;
 constructors FUNCT_4, FUNCOP_1, BINOP_1, GROUP_1, SETWISEO, FILTER_0,
      PARTFUN1, MEMBERED, XBOOLE_0;
 clusters LATTICES, STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Auxiliary theorems

reserve A for set, C for non empty set,
        B for Subset of A,
        x for Element of A,
        f,g for Function of A,C;

canceled;

theorem :: LATTICE2:2
 dom (g|B) = B;

canceled 2;

theorem :: LATTICE2:5
 f|B = g|B iff for x st x in B holds g.x = f.x;

theorem :: LATTICE2:6
 for B being set holds f +* g|B is Function of A,C;

theorem :: LATTICE2:7
  g|B +* f = f;

theorem :: LATTICE2:8
 for f,g being Function holds g <= f implies f +* g = f;

theorem :: LATTICE2:9
 f +* f|B = f;

theorem :: LATTICE2:10
 (for x st x in B holds g.x = f.x) implies f +* g|B = f;

reserve B for Finite_Subset of A;

canceled;

theorem :: LATTICE2:12
g|B +* f = f;

theorem :: LATTICE2:13
dom (g|B) = B;

theorem :: LATTICE2:14
(for x st x in B holds g.x = f.x) implies f +* g|B = f;

canceled;

theorem :: LATTICE2:16
 f|B = g|B implies f.:B = g.:B;

definition let D be non empty set;
 let o,o' be BinOp of D;
  pred o absorbs o' means
:: LATTICE2:def 1
 for x,y being Element of D holds o.(x,o'.(x,y)) = x;
  antonym o doesn't_absorb o';
end;

:: Dual Lattice structures

reserve L for non empty LattStr,
        a,b,c for Element of L;

theorem :: LATTICE2:17
  the L_join of L is commutative associative &
  the L_meet of L is commutative associative &
  the L_join of L absorbs the L_meet of L &
  the L_meet of L absorbs the L_join of L
   implies L is Lattice-like;


definition let L be LattStr;
 func L.: -> strict LattStr equals
:: LATTICE2:def 2
 LattStr(#the carrier of L, the L_meet of L, the L_join of L#);
end;

definition let L be non empty LattStr;
 cluster L.: -> non empty;
end;

theorem :: LATTICE2:18
 the carrier of L = the carrier of L.: &
 the L_join of L = the L_meet of L.: &
 the L_meet of L = the L_join of L.:;

theorem :: LATTICE2:19
   for L being strict non empty LattStr holds L.:.: = L;

:: General Lattices

reserve L for Lattice;
reserve a,b,c,u,v for Element of L;

canceled;

theorem :: LATTICE2:21
 (for v holds u "\/" v = v) implies u = Bottom L;

theorem :: LATTICE2:22
 (for v holds (the L_join of L).(u,v) = v) implies u = Bottom L;

canceled;

theorem :: LATTICE2:24
 (for v holds u "/\" v = v) implies u = Top L;

theorem :: LATTICE2:25
 (for v holds (the L_meet of L).(u,v) = v) implies u = Top L;

theorem :: LATTICE2:26
 the L_join of L is idempotent;

theorem :: LATTICE2:27
 for L being join-commutative (non empty \/-SemiLattStr) holds
  the L_join of L is commutative;

theorem :: LATTICE2:28
 the L_join of L has_a_unity implies Bottom L = the_unity_wrt the L_join of L;

theorem :: LATTICE2:29
 for L being join-associative (non empty \/-SemiLattStr) holds
 the L_join of L is associative;

theorem :: LATTICE2:30
 the L_meet of L is idempotent;

theorem :: LATTICE2:31
 for L being meet-commutative (non empty /\-SemiLattStr) holds
 the L_meet of L is commutative;

theorem :: LATTICE2:32
 for L being meet-associative (non empty /\-SemiLattStr) holds
 the L_meet of L is associative;

definition let L be join-commutative (non empty \/-SemiLattStr);
  cluster the L_join of L -> commutative;
end;

definition let L be join-associative (non empty \/-SemiLattStr);
  cluster the L_join of L -> associative;
end;

definition let L be meet-commutative (non empty /\-SemiLattStr);
  cluster the L_meet of L -> commutative;
end;

definition let L be meet-associative (non empty /\-SemiLattStr);
  cluster the L_meet of L -> associative;
end;

theorem :: LATTICE2:33
 the L_meet of L has_a_unity implies Top L = the_unity_wrt the L_meet of L;

theorem :: LATTICE2:34
 the L_join of L is_distributive_wrt the L_join of L;

theorem :: LATTICE2:35
   L is D_Lattice implies
 the L_join of L is_distributive_wrt the L_meet of L;

theorem :: LATTICE2:36
 the L_join of L is_distributive_wrt the L_meet of L
 implies L is distributive;

theorem :: LATTICE2:37
 L is D_Lattice implies
 the L_meet of L is_distributive_wrt the L_join of L;

theorem :: LATTICE2:38
   the L_meet of L is_distributive_wrt the L_join of L
 implies L is distributive;

theorem :: LATTICE2:39
 the L_meet of L is_distributive_wrt the L_meet of L;

theorem :: LATTICE2:40
  the L_join of L absorbs the L_meet of L;

theorem :: LATTICE2:41
 the L_meet of L absorbs the L_join of L;

definition let A be non empty set, L be Lattice;
 let B be Finite_Subset of A; let f be Function of A, the carrier of L;
  func FinJoin(B, f) -> Element of L equals
:: LATTICE2:def 3
  (the L_join of L)$$(B,f);
  func FinMeet(B, f) -> Element of L equals
:: LATTICE2:def 4
  (the L_meet of L)$$(B,f);
end;

reserve A for non empty set,
        x for Element of A,
        B for Finite_Subset of A,
        f,g for Function of A, the carrier of L;

canceled;

theorem :: LATTICE2:43
  x in B implies f.x [= FinJoin(B,f);

theorem :: LATTICE2:44
  (ex x st x in B & u [= f.x) implies u [= FinJoin(B,f);


theorem :: LATTICE2:45
  (for x st x in B holds f.x = u) & B <> {} implies FinJoin(B,f) = u;

theorem :: LATTICE2:46
     FinJoin(B,f) [= u implies for x st x in B holds f.x [= u;

theorem :: LATTICE2:47
  B <> {} & (for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u;

theorem :: LATTICE2:48
    B <> {} & (for x st x in B holds f.x [= g.x)
   implies FinJoin(B,f) [= FinJoin(B,g);

theorem :: LATTICE2:49
 B <> {} & f|B = g|B implies FinJoin(B,f) = FinJoin(B,g);

theorem :: LATTICE2:50
     B <> {} implies v "\/" FinJoin(B,f) = FinJoin(B, (the L_join of L)[;](v,f)
);

definition let L be Lattice;
 cluster L.: -> Lattice-like;
end;

theorem :: LATTICE2:51
 for L being Lattice,
     B being Finite_Subset of A
 for f being Function of A, the carrier of L,
     f' being Function of A, the carrier of L.: st f = f'
   holds FinJoin(B,f) = FinMeet(B,f') &
         FinMeet(B,f) = FinJoin(B,f');

theorem :: LATTICE2:52
 for a',b' being Element of L.: st a = a' & b = b' holds
  a "/\" b = a'"\/" b' & a "\/" b = a'"/\" b';


theorem :: LATTICE2:53
 a [= b implies
  for a',b' being Element of L.: st a = a' & b = b'
   holds b' [= a';

theorem :: LATTICE2:54
 for a',b' being Element of L.:
   st a' [= b' & a = a' & b = b'
  holds b [= a;

:: Dualizations

theorem :: LATTICE2:55
  x in B implies FinMeet(B,f) [= f.x;

theorem :: LATTICE2:56
  (ex x st x in B & f.x [= u) implies FinMeet(B,f)[= u;

theorem :: LATTICE2:57
    (for x st x in B holds f.x = u) & B <> {} implies FinMeet(B,f) = u;

theorem :: LATTICE2:58
    B <> {} implies v "/\" FinMeet(B,f) = FinMeet(B, (the L_meet of L)[;](v,f))
;

theorem :: LATTICE2:59
    u [= FinMeet(B,f) implies for x st x in B holds u [= f.x;

theorem :: LATTICE2:60
   B <> {} & f|B = g|B implies FinMeet(B,f) = FinMeet(B,g);

theorem :: LATTICE2:61
  B <> {} & (for x st x in B holds u [= f.x) implies u [= FinMeet(B,f);

theorem :: LATTICE2:62
    B <> {} & (for x st x in B holds f.x [= g.x)
   implies FinMeet(B,f) [= FinMeet(B,g);

theorem :: LATTICE2:63
   for L being Lattice holds L is lower-bounded iff L.: is upper-bounded;

theorem :: LATTICE2:64
 for L being Lattice holds L is upper-bounded iff L.: is lower-bounded;

theorem :: LATTICE2:65
   L is D_Lattice iff L.: is D_Lattice;

:::::::::::::::::::::::::::
::
:: Lower bounded lattices
::
:::::::::::::::::::::::::::

reserve L for 0_Lattice,
        f,g for Function of A, the carrier of L,
        u for Element of L;

theorem :: LATTICE2:66
 Bottom L is_a_unity_wrt the L_join of L;

theorem :: LATTICE2:67
 the L_join of L has_a_unity;

theorem :: LATTICE2:68
 Bottom L = the_unity_wrt the L_join of L;

theorem :: LATTICE2:69
 f|B = g|B implies FinJoin(B,f) = FinJoin(B,g);

theorem :: LATTICE2:70
  (for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u;

theorem :: LATTICE2:71
    (for x st x in B holds f.x [= g.x)
   implies FinJoin(B,f) [= FinJoin(B,g);

:::::::::::::::::::::::::::
::
:: Upper bounded lattices
::
:::::::::::::::::::::::::::

reserve L for 1_Lattice,
        f,g for Function of A, the carrier of L,
        u for Element of L;

theorem :: LATTICE2:72
 Top L is_a_unity_wrt the L_meet of L;

theorem :: LATTICE2:73
 the L_meet of L has_a_unity;

theorem :: LATTICE2:74
   Top L = the_unity_wrt the L_meet of L;

theorem :: LATTICE2:75
   f|B = g|B implies FinMeet(B,f) = FinMeet(B,g);

theorem :: LATTICE2:76
  (for x st x in B holds u [= f.x) implies u [= FinMeet(B,f);

theorem :: LATTICE2:77
    (for x st x in B holds f.x [= g.x)
   implies FinMeet(B,f) [= FinMeet(B,g);

theorem :: LATTICE2:78
   for L being 0_Lattice holds Bottom L = Top (L.:);

theorem :: LATTICE2:79
   for L being 1_Lattice holds Top L = Bottom (L.:);

:::::::::::::::::::::::::::
::
:: Distributive lattices with the minimal element
::
:::::::::::::::::::::::::::

definition
  mode D0_Lattice is distributive lower-bounded Lattice;
end;

reserve L for D0_Lattice,
        f,g for (Function of A, the carrier of L),
        u for Element of L;

theorem :: LATTICE2:80
   the L_meet of L is_distributive_wrt the L_join of L;

theorem :: LATTICE2:81
  (the L_meet of L).(u, FinJoin(B, f))
         = FinJoin(B, (the L_meet of L)[;](u,f));

theorem :: LATTICE2:82
    (for x st x in B holds g.x = u "/\" f.x)
     implies u "/\" FinJoin(B,f) = FinJoin(B,g);

theorem :: LATTICE2:83
  u "/\" FinJoin(B,f) = FinJoin(B, (the L_meet of L)[;](u, f));

:: Heyting Lattices

definition
 let IT be Lattice;
 canceled;

  attr IT is Heyting means
:: LATTICE2:def 6
 IT is implicative lower-bounded;
end;

definition
  cluster Heyting Lattice;
end;

definition
 cluster Heyting -> implicative lower-bounded Lattice;
 cluster implicative lower-bounded -> Heyting Lattice;
end;

definition
  mode H_Lattice is Heyting Lattice;
end;

definition
 cluster Heyting strict Lattice;
end;

theorem :: LATTICE2:84
   for L being 0_Lattice holds
  L is H_Lattice iff
  for x,z being Element of L
   ex y being Element of L st x "/\" y [= z
    & for v being Element of L st x "/\" v [= z holds v [= y;

theorem :: LATTICE2:85
   for L being Lattice holds L is finite iff L.: is finite;

definition
 cluster finite -> lower-bounded Lattice;
 cluster finite -> upper-bounded Lattice;
end;

definition
 cluster finite -> bounded Lattice;
end;

definition
 cluster distributive finite -> Heyting Lattice;
end;