Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Homomorphisms of Lattices, Finite Join and Finite Meet

by
Jolanta Kamienska, and
Jaroslaw Stanislaw Walijewski

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;
```