:: Homomorphisms of Lattices \\ Finite Join and Finite Meet
:: by Jolanta Kamie\'nska and Jaros\l aw Stanis\l aw Walijewski
::
:: Received July 14, 1993
:: Copyright (c) 1993-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, TARSKI, ORDINAL1, SUBSET_1, LATTICES, CARD_FIL,
FILTER_0, INT_2, PBOOLE, GROUP_6, FUNCT_1, STRUCT_0, EQREL_1, FUNCT_2,
RELAT_1, WELLORD1, FILTER_1, XBOOLEAN, FINSUB_1, LATTICE2, SETWISEO,
BINOP_1, FUNCOP_1, XXREAL_2, VECTSP_1, ZFMISC_1, SETFAM_1, LATTICE4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, LATTICES,
LATTICE2, FILTER_0, FUNCOP_1, SETWISEO, WELLORD1, FILTER_1;
constructors WELLORD1, DOMAIN_1, SETWISEO, LATTICE2, FILTER_1, GRCAT_1,
FUNCOP_1, RELSET_1, FILTER_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICES,
LATTICE2;
requirements BOOLE, SUBSET;
begin :: Preliminaries
reserve x,y,X,X1,Y,Z for set;
theorem :: LATTICE4:1
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;
registration
let L;
cluster <.L.) -> prime;
end;
theorem :: LATTICE4:2
F c= <.F \/ H.) & H c= <.F \/ H.);
theorem :: LATTICE4:3
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:4
a1 [= b1 implies f.a1 [= f.b1;
theorem :: LATTICE4:5
f is one-to-one implies (a1 [= b1 iff (f.a1) [= (f.b1));
theorem :: LATTICE4:6
for f being Function of the carrier of L1, the carrier of L2
holds f is onto implies for a2 ex a1 st a2 = f.a1;
definition
let L1,L2;
redefine pred L1,L2 are_isomorphic means
:: LATTICE4:def 2
ex f st f is bijective;
end;
definition
let L1,L2,f;
pred f preserves_implication means
:: LATTICE4:def 3
f.(a1 => b1) = (f.a1) => (f.b1);
pred f preserves_top means
:: LATTICE4:def 4
f.(Top L1) = Top L2;
pred f preserves_bottom means
:: LATTICE4:def 5
f.(Bottom L1) = Bottom L2;
pred f preserves_complement means
:: LATTICE4:def 6
f.(a1`) = (f.a1)`;
end;
definition
let L;
mode ClosedSubset of L is meet-closed join-closed Subset of L;
end;
theorem :: LATTICE4:7
the carrier of L is ClosedSubset of L;
registration
let L;
cluster non empty for ClosedSubset of L;
end;
theorem :: LATTICE4:8
for F being Filter of L holds F is ClosedSubset of L;
reserve B for Element of Fin the carrier of L;
definition
let L,B;
func FinJoin B -> Element of L equals
:: LATTICE4:def 7
FinJoin (B,id L);
func FinMeet B -> Element of L equals
:: LATTICE4:def 8
FinMeet (B,id L);
end;
theorem :: LATTICE4:9
FinJoin {.p.} = p;
theorem :: LATTICE4:10
FinMeet {.p.} = p;
begin :: Distributive Lattices
reserve DL for distributive Lattice;
reserve f for Homomorphism of DL,L2;
theorem :: LATTICE4:11
f is onto implies L2 is distributive;
begin :: Lower-bounded Lattices
reserve 0L for lower-bounded Lattice,
B,B1,B2 for Element of Fin the carrier of 0L,
b for Element of 0L;
theorem :: LATTICE4:12
for f being Homomorphism of 0L,L2 st f is onto holds L2 is
lower-bounded & f preserves_bottom;
reserve f for UnOp of the carrier of 0L;
theorem :: LATTICE4:13
FinJoin(B \/ {.b.},f) = FinJoin (B,f) "\/" f.b;
theorem :: LATTICE4:14
FinJoin(B \/ {.b.}) = FinJoin B "\/" b;
theorem :: LATTICE4:15
FinJoin B1 "\/" FinJoin B2 = FinJoin (B1 \/ B2);
theorem :: LATTICE4:16
FinJoin {}.the carrier of 0L = Bottom 0L;
theorem :: LATTICE4:17
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 Element of Fin the carrier of 1L,
b for Element of 1L;
theorem :: LATTICE4:18
for f being Homomorphism of 1L,L2 st f is onto holds L2 is
upper-bounded & f preserves_top;
theorem :: LATTICE4:19
FinMeet {}.the carrier of 1L = Top 1L;
reserve f,g for UnOp of the carrier of 1L;
theorem :: LATTICE4:20
FinMeet(B \/ {.b.},f) = FinMeet (B,f) "/\" f.b;
theorem :: LATTICE4:21
FinMeet(B \/ {.b.}) = FinMeet B "/\" b;
theorem :: LATTICE4:22
FinMeet(f.:B,g) = FinMeet(B,g*f);
theorem :: LATTICE4:23
FinMeet B1 "/\" FinMeet B2 = FinMeet (B1 \/ B2);
theorem :: LATTICE4:24
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 Element of Fin the carrier of DL,
p for Element of DL,
f for UnOp of the carrier of DL;
theorem :: LATTICE4:25
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:26
f.i "/\" f.(i => j) [= f.j;
theorem :: LATTICE4:27
f is one-to-one implies (f.i "/\" f.k [= f.j implies f.k [= f.(i => j));
theorem :: LATTICE4:28
f is bijective 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,A1,A2 for Element of Fin the carrier of BL;
theorem :: LATTICE4:29
(Top BL)`=Bottom BL;
theorem :: LATTICE4:30
(Bottom BL)`=Top BL;
theorem :: LATTICE4:31
f is onto implies CL is Boolean & f preserves_complement;
definition
let BL;
mode Field of BL -> non empty Subset of BL means
:: LATTICE4:def 9
a in it & b in it implies a "/\" b in it & a` in it;
end;
reserve F,H for Field of BL;
theorem :: LATTICE4:32
a in F & b in F implies a "\/" b in F;
theorem :: LATTICE4:33
a in F & b in F implies a => b in F;
theorem :: LATTICE4:34
the carrier of BL is Field of BL;
theorem :: LATTICE4:35
F is ClosedSubset of BL;
definition
let BL,A;
func field_by A -> Field of BL means
:: LATTICE4:def 10
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 11
{ a => b : a in A & b in A};
end;
registration
let BL,A;
cluster SetImp A -> non empty;
end;
theorem :: LATTICE4:36
x in SetImp A iff ex p,q st x = p => q & p in A & q in A;
theorem :: LATTICE4:37
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 12
it.a = a`;
end;
theorem :: LATTICE4:38
FinJoin(B \/ {.b.},comp BL) = FinJoin (B,comp BL) "\/" b`;
theorem :: LATTICE4:39
(FinJoin B)` = FinMeet (B,comp BL);
theorem :: LATTICE4:40
FinMeet(B \/ {.b.},comp BL) = FinMeet (B,comp BL) "/\" b`;
theorem :: LATTICE4:41
(FinMeet B)` = FinJoin (B,comp BL);
theorem :: LATTICE4:42
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:43
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;