The Mizar abstract of LATTICE4

Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users
The abstract of the Mizar article:: Homomorphisms of Lattices, Finite Join and Finite Meet
by
Jolanta Kamienska, and
Jaroslaw Stanislaw Walijewski
Received July 14, 1993
MML identifier: LATTICE4
[ Mizar article, MML identifier index ]
environ

 vocabulary TARSKI, SETFAM_1, BOOLE, LATTICES, FILTER_0, GROUP_6, FUNCT_1,
      MOD_4, RELAT_1, WELLORD1, FILTER_1, ZF_LANG, SUBSET_1, FINSUB_1,
      LATTICE2, SETWISEO, BINOP_1, FUNCOP_1, VECTSP_1, LATTICE4, HAHNBAN;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
      FUNCT_1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, LATTICES, LATTICE2,
      FILTER_0, FUNCOP_1, SETWISEO, GRCAT_1, WELLORD1, FILTER_1;
 constructors BINOP_1, LATTICE2, SETWISEO, GRCAT_1, WELLORD1, FILTER_1,
      DOMAIN_1, XBOOLE_0, TOPS_2;
 clusters LATTICES, FILTER_0, STRUCT_0, FINSUB_1, RELSET_1, SUBSET_1, XBOOLE_0,
      ZFMISC_1;
 requirements BOOLE, SUBSET;


begin :: Preliminaries

reserve x,y,X,X1,Y,Z for set;

theorem :: LATTICE4:1
   union Y c= Z & X in Y implies X c= Z;

theorem :: LATTICE4:2
    union INTERSECTION(X,Y) = union X /\ union Y;

theorem :: LATTICE4:3
    for X st X <> {} &
   for Z st Z <> {} & Z c= X &
    Z is c=-linear
     ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y
   ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z;

begin :: Lattice Theory

reserve L for Lattice;
reserve F,H for Filter of L;
reserve p,q,r for Element of L;

theorem :: LATTICE4:4
    <.L.) is prime;

theorem :: LATTICE4:5
   F c= <.F \/ H.) & H c= <.F \/ H.);

theorem :: LATTICE4:6
    p in <.<.q.) \/ F.) implies ex r st r in F & q "/\" r [= p;

reserve L1, L2 for Lattice;
reserve a1,b1 for Element of L1;
reserve a2 for Element of L2;

definition let L1,L2;
 mode Homomorphism of L1,L2 ->
  Function of the carrier of L1, the carrier of L2 means
:: LATTICE4:def 1
  it.(a1 "\/" b1) = it.a1 "\/" it.b1 &
       it.(a1 "/\" b1) = it.a1 "/\" it.b1;
end;

reserve f for Homomorphism of L1,L2;

theorem :: LATTICE4:7
 a1 [= b1 implies f.a1 [= f.b1;

definition let L1,L2;
           let f be Function of the carrier of L1, the carrier of L2;
 attr f is monomorphism means
:: LATTICE4:def 2
     f is one-to-one;
 attr f is epimorphism means
:: LATTICE4:def 3
     rng f = the carrier of L2;
end;

theorem :: LATTICE4:8
 f is monomorphism implies (a1 [= b1 iff (f.a1) [= (f.b1));

theorem :: LATTICE4:9
 for f being Function of the carrier of L1, the carrier of L2 holds
  f is epimorphism implies (for a2 ex a1 st a2 = f.a1);

definition
  let L1,L2,f;
 attr f is isomorphism means
:: LATTICE4:def 4
    f is monomorphism epimorphism;
end;

definition let L1,L2;
 redefine pred L1,L2 are_isomorphic means
:: LATTICE4:def 5
      ex f st f is isomorphism;
end;

definition
let L1,L2,f;
 pred f preserves_implication means
:: LATTICE4:def 6
     f.(a1 => b1) = (f.a1) => (f.b1);
 pred f preserves_top means
:: LATTICE4:def 7
     f.(Top L1) = Top L2;
 pred f preserves_bottom means
:: LATTICE4:def 8
     f.(Bottom L1) = Bottom L2;
 pred f preserves_complement means
:: LATTICE4:def 9
     f.(a1`) = (f.a1)`;
end;

definition let L;
 mode ClosedSubset of L -> Subset of L means
:: LATTICE4:def 10
  p in it & q in it implies p "/\" q in it & p "\/" q in it;
end;

theorem :: LATTICE4:10
  the carrier of L is ClosedSubset of L;

definition let L;
 cluster non empty ClosedSubset of L;
end;

theorem :: LATTICE4:11
    for F being Filter of L holds F is ClosedSubset of L;

 reserve B for Finite_Subset of the carrier of L;

definition let L,B;
 canceled;

  func FinJoin B -> Element of L equals
:: LATTICE4:def 12
   FinJoin (B,id L);
  func FinMeet B -> Element of L equals
:: LATTICE4:def 13
   FinMeet (B,id L);
end;

canceled 2;

theorem :: LATTICE4:14
  FinMeet B = (the L_meet of L) $$ (B,id L);

theorem :: LATTICE4:15
   FinJoin B = (the L_join of L) $$ (B,id L);

theorem :: LATTICE4:16
  FinJoin {p} = p;

theorem :: LATTICE4:17
 FinMeet {p} = p;

begin :: Distributive Lattices

reserve DL for distributive Lattice;
reserve f for Homomorphism of DL,L2;

theorem :: LATTICE4:18
  f is epimorphism implies L2 is distributive;

begin :: Lower-bounded Lattices

reserve 0L for lower-bounded Lattice,
        B,B1,B2 for Finite_Subset of the carrier of 0L,
        b for Element of 0L;

theorem :: LATTICE4:19
 for f being Homomorphism of 0L,L2 st f is epimorphism
  holds L2 is lower-bounded & f preserves_bottom;

reserve f for UnOp of the carrier of 0L;

theorem :: LATTICE4:20
  FinJoin(B \/ {b},f) = FinJoin (B,f) "\/" f.b;

theorem :: LATTICE4:21
  FinJoin(B \/ {b}) = FinJoin B "\/" b;

 theorem :: LATTICE4:22
    FinJoin B1 "\/" FinJoin B2 = FinJoin (B1 \/ B2);

theorem :: LATTICE4:23
  FinJoin {}.the carrier of 0L = Bottom 0L;

theorem :: LATTICE4:24
  for A being ClosedSubset of 0L st Bottom 0L in A
            for B holds B c= A implies FinJoin B in A;

begin :: Upper-bounded Lattices

reserve 1L for upper-bounded Lattice,
        B,B1,B2 for Finite_Subset of the carrier of 1L,
        b for Element of 1L;

theorem :: LATTICE4:25
  for f being Homomorphism of 1L,L2 st f is epimorphism
   holds L2 is upper-bounded & f preserves_top;

theorem :: LATTICE4:26
  FinMeet {}.the carrier of 1L = Top 1L;

reserve f,g for UnOp of the carrier of 1L;

theorem :: LATTICE4:27
   FinMeet(B \/ {b},f) = FinMeet (B,f) "/\" f.b;

theorem :: LATTICE4:28
  FinMeet(B \/ {b}) = FinMeet B "/\" b;

theorem :: LATTICE4:29
  FinMeet(f.:B,g) = FinMeet(B,g*f);

theorem :: LATTICE4:30
 FinMeet B1 "/\" FinMeet B2 = FinMeet (B1 \/ B2);

theorem :: LATTICE4:31
 for F being ClosedSubset of 1L st Top 1L in F
         for B holds B c= F implies FinMeet B in F;

begin :: Distributive Upper-bounded Lattices

 reserve DL for distributive upper-bounded Lattice,
         B for Finite_Subset of the carrier of DL,
         p for Element of DL,
         f for UnOp of the carrier of DL;

theorem :: LATTICE4:32
 FinMeet B "\/" p = FinMeet (((the L_join of DL)[:](id DL,p)).:B);

begin :: Implicative Lattices

reserve CL for C_Lattice;
reserve IL for implicative Lattice;
reserve f for Homomorphism of IL,CL;
reserve i,j,k for Element of IL;

theorem :: LATTICE4:33
  f.i "/\" f.(i => j) [= f.j;

theorem :: LATTICE4:34
  f is monomorphism implies (f.i "/\" f.k [= f.j implies f.k [= f.(i => j));

theorem :: LATTICE4:35
  f is isomorphism implies (CL is implicative & f preserves_implication);

begin ::Boolean Lattices

reserve BL for Boolean Lattice;
reserve f for Homomorphism of BL,CL;
reserve A for non empty Subset of BL;
reserve a1,a,b,c,p,q for Element of BL;
reserve B,B0,B1,B2,B3,A1,A2 for Finite_Subset of the carrier of BL;

theorem :: LATTICE4:36
  (Top BL)`=Bottom BL;

theorem :: LATTICE4:37
  (Bottom BL)`=Top BL;

theorem :: LATTICE4:38
    f is epimorphism implies CL is Boolean & f preserves_complement;

definition let BL;
 mode Field of BL -> non empty Subset of BL means
:: LATTICE4:def 14
   a in it & b in it implies a "/\" b in it & a` in it;
end;

reserve F,H for Field of BL;

theorem :: LATTICE4:39
  a in F & b in F implies a "\/" b in F;

theorem :: LATTICE4:40
  a in F & b in F implies a => b in F;

theorem :: LATTICE4:41
  the carrier of BL is Field of BL;

theorem :: LATTICE4:42
  F is ClosedSubset of BL;

definition let BL,A;
 func field_by A -> Field of BL means
:: LATTICE4:def 15
   A c= it & for F st A c= F holds it c= F;
end;

definition let BL,A;
 func SetImp A -> Subset of BL equals
:: LATTICE4:def 16
   { a => b : a in A & b in A};
end;

definition let BL,A;
 cluster SetImp A -> non empty;
end;

theorem :: LATTICE4:43
  x in SetImp A iff ex p,q st x = p => q & p in A & q in A;

theorem :: LATTICE4:44
c in SetImp A iff ex p,q st c = p` "\/" q & p in A & q in A;

definition let BL;
 func comp BL -> Function of the carrier of BL, the carrier of BL means
:: LATTICE4:def 17

     it.a = a`;
 end;

theorem :: LATTICE4:45
 FinJoin(B \/ {b},comp BL) = FinJoin (B,comp BL) "\/" b`;

theorem :: LATTICE4:46
    (FinJoin B)` = FinMeet (B,comp BL);

theorem :: LATTICE4:47
    FinMeet(B \/ {b},comp BL) = FinMeet (B,comp BL) "/\" b`;

theorem :: LATTICE4:48
 (FinMeet B)` = FinJoin (B,comp BL);

theorem :: LATTICE4:49
   for AF  being non empty ClosedSubset of BL st Bottom
BL in AF & Top BL in AF
     for B holds B c= SetImp AF implies
         ex B0 st B0 c= SetImp AF & FinJoin( B,comp BL) = FinMeet B0;

theorem :: LATTICE4:50
    for AF being non empty ClosedSubset of BL st Bottom
BL in AF & Top BL in AF holds
    { FinMeet B : B c= SetImp AF } = field_by AF;
The abstract of the Mizar article:

Homomorphisms of Lattices, Finite Join and Finite Meet
