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;

Back to top