:: 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-2026 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;
definitions TARSKI, FILTER_0, LATTICES, XBOOLE_0;
equalities FILTER_0, LATTICES, STRUCT_0;
expansions TARSKI, FILTER_0, LATTICES;
theorems LATTICES, ZFMISC_1, FUNCT_2, FILTER_0, SETFAM_1, ORDERS_1, TARSKI,
SETWISEO, LATTICE2, FUNCOP_1, FILTER_1, WELLORD1, RELAT_1, XBOOLE_1,
FUNCT_1, GROUP_6;
schemes FUNCT_2, SETWISEO, BINOP_2, XFAMILY;
begin :: Preliminaries
reserve x,y,X,X1,Y,Z for set;
theorem
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
proof
let X such that
A1: X <> {} and
A2: 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;
for Z st Z c= X & Z is c=-linear ex Y st Y in X & for X1 st X1 in Z
holds X1 c= Y
proof
let Z such that
A3: Z c= X & Z is c=-linear;
per cases;
suppose
A4: Z = {};
set Y = the Element of X;
for X1 st X1 in Z holds X1 c= Y by A4;
hence thesis by A1;
end;
suppose
Z <> {};
hence thesis by A2,A3;
end;
end;
hence thesis by A1,ORDERS_1:65;
end;
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;
coherence;
end;
theorem
F c= <.F \/ H.) & H c= <.F \/ H.)
proof
A1: F \/ H c= <.F \/ H.) by FILTER_0:def 4;
F c= F \/ H & H c= F \/ H by XBOOLE_1:7;
hence thesis by A1;
end;
theorem
p in <.<.q.) \/ F.) implies ex r st r in F & q "/\" r [= p
proof
A1: <.<.q.) \/ F.)={r : ex p9,q9 being Element of L st p9"/\"q9 [= r & p9 in
<.q.) & q9 in F} by FILTER_0:35;
assume p in <.<.q.) \/ F.);
then
ex r st r=p & ex p9,q9 being Element of L st p9"/\"q9 [= r & p9 in <.q.)
& q9 in F by A1;
then consider p9,q9 being Element of L such that
A2: p9 "/\" q9 [= p and
A3: p9 in <.q.) and
A4: q9 in F;
q [= p9 by A3,FILTER_0:15;
then q "/\" q9 [= p9 "/\" q9 by LATTICES:9;
hence thesis by A2,A4,LATTICES:7;
end;
reserve L1, L2 for Lattice;
reserve a1,b1 for Element of L1;
reserve a2 for Element of L2;
definition
let L1,L2 be non empty \/-SemiLattStr;
let f be Function of L1,L2;
attr f is "\/"-preserving means :D1:
for a,b being Element of L1 holds f.(a"\/"b) = f.a "\/" f.b;
end;
definition
let L1,L2 be non empty /\-SemiLattStr;
let f be Function of L1,L2;
attr f is "/\"-preserving means :D2:
for a,b being Element of L1 holds f.(a"/\"b) = f.a "/\" f.b;
end;
registration
let L1,L2 be meet-absorbing join-absorbing meet-commutative
non empty LattStr;
cluster "\/"-preserving "/\"-preserving for Function of L1,L2;
existence
proof
set b = the Element of L2;
defpred P[set,set] means
for a1 being Element of L1 st $1=a1 holds $2=b;
A1: now
let x be Element of L1;
take b;
thus P[x,b];
end;
consider f being Function of L1,L2 such that
A2: for x being Element of L1 holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
thus f is "\/"-preserving
proof
let a1,b1 be Element of L1;
thus f.(a1 "\/" b1) = b by A2
.= b "\/" b
.= f.a1 "\/" b by A2
.= f.a1 "\/" f.b1 by A2;
end;
let a1,b1 be Element of L1;
thus f.(a1 "/\" b1) = b by A2
.= b "/\" b
.= f.a1 "/\" b by A2
.= f.a1 "/\" f.b1 by A2;
end;
end;
definition
let L1,L2 be Lattice;
mode Homomorphism of L1,L2
is "\/"-preserving "/\"-preserving Function of L1,L2;
end;
reserve f for Homomorphism of L1,L2;
theorem Th4:
a1 [= b1 implies f.a1 [= f.b1 by D1;
theorem Th5:
f is one-to-one implies (a1 [= b1 iff (f.a1) [= (f.b1))
proof
assume
A1: f is one-to-one;
reconsider f as Function of L1,L2;
f.a1 [= f.b1 implies a1 [= b1
proof
assume f.a1 [= f.b1;
then f.(a1 "\/" b1) = f.b1 by D1;
hence a1 "\/" b1 = b1 by A1,FUNCT_2:19;
end;
hence thesis by Th4;
end;
theorem Th6: ::: GROUP_6:58
for f being Function of L1,L2
holds f is onto implies for a2 being Element of L2
ex a1 being Element of L1 st a2 = f.a1
by GROUP_6:58;
definition
let L1,L2;
redefine pred L1,L2 are_isomorphic means :: redefines are_isomorphic (FILTER_1, definition)
ex f st f is bijective;
compatibility
proof
thus L1,L2 are_isomorphic implies ex f st f is bijective
proof
set R = LattRel L1, S = LattRel L2;
assume L1,L2 are_isomorphic;
then LattRel L1, LattRel L2 are_isomorphic by FILTER_1:def 9;
then consider F being Function such that
A1: F is_isomorphism_of LattRel L1, LattRel L2 by WELLORD1:def 8;
A2: dom F = field R by A1,WELLORD1:def 7;
A3: field S = the carrier of L2 & rng F = field S by A1,FILTER_1:32
,WELLORD1:def 7;
A4: field R = the carrier of L1 by FILTER_1:32;
then reconsider F as Function of L1,L2 by A2,A3,FUNCT_2:1;
now
let a1,b1 be Element of L1;
reconsider a19=a1,b19=b1 as Element of L1;
A5: F is onto by A3,FUNCT_2:def 3;
thus F.(a1 "\/" b1) = F.a1 "\/" F.b1
proof
b19 [= a19 "\/" b19 by LATTICES:5;
then [b1,a1 "\/" b1] in R by FILTER_1:31;
then [F.b1,F.(a1 "\/" b1)] in S by A1,WELLORD1:def 7;
then
A6: F.b19 [= F.(a19 "\/" b19) by FILTER_1:31;
consider k1 being Element of L1 such that
A7: F.a1 "\/" F.b1 = F.k1 by A5,Th6;
F.b1 [= F.k1 by A7,LATTICES:5;
then [F.b1,F.k1] in LattRel L2 by FILTER_1:31;
then [b1,k1] in LattRel L1 by A1,A4,WELLORD1:def 7;
then
A8: b1 [= k1 by FILTER_1:31;
F.a1 [= F.k1 by A7,LATTICES:5;
then [F.a1,F.k1] in LattRel L2 by FILTER_1:31;
then [a1,k1] in LattRel L1 by A1,A4,WELLORD1:def 7;
then a1 [= k1 by FILTER_1:31;
then a1 "\/" b1 [= k1 by A8,FILTER_0:6;
then [a1 "\/" b1,k1] in R by FILTER_1:31;
then [F.(a1 "\/" b1),F.k1] in LattRel L2 by A1,WELLORD1:def 7;
then
A9: F.(a1 "\/" b1) [= F.a1 "\/" F.b1 by A7,FILTER_1:31;
a19 [= a19 "\/" b19 by LATTICES:5;
then [a1,a1 "\/" b1] in R by FILTER_1:31;
then [F.a1,F.(a1 "\/" b1)] in S by A1,WELLORD1:def 7;
then F.a19 [= F.(a19 "\/" b19) by FILTER_1:31;
then F.a1 "\/" F.b1 [= F.(a1 "\/" b1) by A6,FILTER_0:6;
hence thesis by A9,LATTICES:8;
end;
thus F.(a1 "/\" b1) = F.a1 "/\" F.b1
proof
a19 "/\" b19 [= b19 by LATTICES:6;
then [a1 "/\" b1,b1] in R by FILTER_1:31;
then [F.(a1 "/\" b1),F.b1] in S by A1,WELLORD1:def 7;
then
A10: F.(a19 "/\" b19) [= F.b19 by FILTER_1:31;
consider k1 being Element of L1 such that
A11: F.a1 "/\" F.b1 = F.k1 by A5,Th6;
F.k1 [= F.b1 by A11,LATTICES:6;
then [F.k1,F.b1] in LattRel L2 by FILTER_1:31;
then [k1,b1] in LattRel L1 by A1,A4,WELLORD1:def 7;
then
A12: k1 [= b1 by FILTER_1:31;
F.k1 [= F.a1 by A11,LATTICES:6;
then [F.k1,F.a1] in LattRel L2 by FILTER_1:31;
then [k1,a1] in LattRel L1 by A1,A4,WELLORD1:def 7;
then k1 [= a1 by FILTER_1:31;
then k1 [= a1 "/\" b1 by A12,FILTER_0:7;
then [k1,a1 "/\" b1] in LattRel L1 by FILTER_1:31;
then [F.k1,F.(a1 "/\" b1)] in LattRel L2 by A1,WELLORD1:def 7;
then
A13: F.a1 "/\" F.b1 [= F.(a1 "/\" b1) by A11,FILTER_1:31;
a19 "/\" b19 [= a19 by LATTICES:6;
then [a1 "/\" b1,a1] in R by FILTER_1:31;
then [F.(a1 "/\" b1),F.a1] in S by A1,WELLORD1:def 7;
then F.(a19 "/\" b19) [= F.a19 by FILTER_1:31;
then F.(a1 "/\" b1) [= F.a1 "/\" F.b1 by A10,FILTER_0:7;
hence thesis by A13,LATTICES:8;
end;
end;
then F is "\/"-preserving "/\"-preserving;
then reconsider F as Homomorphism of L1,L2;
take F;
F is one-to-one onto by A1,A3,FUNCT_2:def 3,WELLORD1:def 7;
hence thesis;
end;
set R = LattRel L1, S = LattRel L2;
given f such that
A14: f is bijective;
A15: for a,b be object holds [a,b] in R iff a in field R & b in field R & [f.
a,f.b] in S
proof
let a,b be object;
hereby
assume
A16: [a,b] in R;
hence a in field R & b in field R by RELAT_1:15;
then reconsider a9=a,b9=b as Element of L1 by FILTER_1:32;
a9 [= b9 by A16,FILTER_1:31;
then f.a9 [= f.b9 by A14,Th5;
hence [f.a,f.b] in S by FILTER_1:31;
end;
assume that
A17: a in field R & b in field R and
A18: [f.a,f.b] in S;
reconsider a9=a,b9=b as Element of L1 by A17,FILTER_1:32;
f.a9 [= f.b9 by A18,FILTER_1:31;
then a9 [= b9 by A14,Th5;
hence thesis by FILTER_1:31;
end;
A19: dom f = the carrier of L1 by FUNCT_2:def 1
.= field R by FILTER_1:32;
rng f = the carrier of L2 by A14,FUNCT_2:def 3
.= field S by FILTER_1:32;
then f is_isomorphism_of LattRel L1, LattRel L2 by A14,A19,A15,
WELLORD1:def 7;
then LattRel L1, LattRel L2 are_isomorphic by WELLORD1:def 8;
hence thesis by FILTER_1:def 9;
end;
end;
definition
let L1,L2,f;
pred f preserves_implication means
f.(a1 => b1) = (f.a1) => (f.b1);
pred f preserves_top means
f.(Top L1) = Top L2;
pred f preserves_bottom means
f.(Bottom L1) = Bottom L2;
pred f preserves_complement means
f.(a1`) = (f.a1)`;
end;
definition
let L;
mode ClosedSubset of L is meet-closed join-closed Subset of L;
end;
theorem Th7:
the carrier of L is ClosedSubset of L
proof
the carrier of L c= the carrier of L;
then reconsider F=the carrier of L as Subset of L;
A1: p in F & q in F implies p "/\" q in F;
p in F & q in F implies p "\/" q in F;
hence thesis by A1,LATTICES:def 24,def 25;
end;
registration
let L;
cluster non empty for ClosedSubset of L;
existence
proof
the carrier of L is ClosedSubset of L by Th7;
hence thesis;
end;
end;
theorem
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
FinJoin (B,id L);
coherence;
func FinMeet B -> Element of L equals
FinMeet (B,id L);
coherence;
end;
theorem Th9:
FinJoin {.p.} = p
proof
thus FinJoin {.p.} =(the L_join of L) $$ ({.p.},id L) by LATTICE2:def 3
.= (id L).p by SETWISEO:17
.= p by FUNCT_1:18;
end;
theorem Th10:
FinMeet {.p.} = p
proof
set M = the L_meet of L;
thus FinMeet {.p.} = M $$ ({.p.},id L) by LATTICE2:def 4
.= (id L).p by SETWISEO:17
.= p by FUNCT_1:18;
end;
begin :: Distributive Lattices
reserve DL for distributive Lattice;
reserve f for Homomorphism of DL,L2;
theorem Th11:
f is onto implies L2 is distributive
proof
assume
A1: f is onto;
thus L2 is distributive
proof
let a,b,c be Element of L2;
consider a9 be Element of DL such that
A2: f.a9=a by A1,Th6;
consider c9 be Element of DL such that
A3: f.c9=c by A1,Th6;
consider b9 be Element of DL such that
A4: f.b9=b by A1,Th6;
thus a"/\"(b"\/"c) = a"/\"f.(b9"\/"c9) by A4,A3,D1
.= f.(a9"/\"(b9"\/"c9)) by A2,D2
.=f.((a9"/\"b9)"\/"(a9"/\"c9)) by LATTICES:def 11
.=f.(a9"/\"b9)"\/"f.(a9"/\"c9) by D1
.=(a"/\"b)"\/"f.(a9"/\"c9) by A2,A4,D2
.=(a"/\"b)"\/"(a"/\"c) by A2,A3,D2;
end;
end;
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 Th12:
for f being Homomorphism of 0L,L2 st f is onto holds
L2 is lower-bounded & f preserves_bottom
proof
let f be Homomorphism of 0L,L2;
set r = f.(Bottom 0L);
assume
A1: f is onto;
A2: now
let a2 be Element of L2;
consider a1 be Element of 0L such that
A3: f.a1 = a2 by A1,Th6;
thus r"/\"a2 = f.(Bottom 0L "/\" a1) by A3,D2
.= r;
hence a2"/\"r = r;
end;
thus L2 is lower-bounded
by A2;
then Bottom L2=r by A2,LATTICES:def 16;
hence thesis;
end;
reserve f for UnOp of the carrier of 0L;
theorem Th13:
FinJoin(B \/ {.b.},f) = FinJoin (B,f) "\/" f.b
proof
set J= the L_join of 0L;
thus FinJoin (B \/ {.b.},f) = J $$ (B \/ {.b.},f) by LATTICE2:def 3
.= J $$ (B,f) "\/" f.b by SETWISEO:32
.= FinJoin (B,f) "\/" f.b by LATTICE2:def 3;
end;
theorem Th14:
FinJoin(B \/ {.b.}) = FinJoin B "\/" b
proof
thus FinJoin(B \/ {.b.}) =FinJoin (B,id 0L) "\/" (id 0L).b by Th13
.= FinJoin B "\/" b by FUNCT_1:18;
end;
theorem
FinJoin B1 "\/" FinJoin B2 = FinJoin (B1 \/ B2)
proof
set J = the L_join of 0L;
thus FinJoin (B1 \/ B2) = J $$ (B1 \/ B2,id 0L) by LATTICE2:def 3
.= J $$ (B1,id 0L) "\/" J $$ (B2,id 0L) by SETWISEO:33
.= FinJoin B1 "\/" J $$ (B2,id 0L) by LATTICE2:def 3
.=FinJoin B1 "\/" FinJoin B2 by LATTICE2:def 3;
end;
Lm1: for f being Function of 0L,0L holds
FinJoin ({}.the carrier of 0L,f) = Bottom 0L
proof
let f be Function of 0L, 0L;
set J=the L_join of 0L;
thus FinJoin ({}.the carrier of 0L,f) = J $$ ({}.the carrier of 0L,f) by
LATTICE2:def 3
.= the_unity_wrt J by SETWISEO:31
.= Bottom 0L by LATTICE2:52;
end;
theorem
FinJoin {}.the carrier of 0L = Bottom 0L by Lm1;
theorem Th17:
for A being ClosedSubset of 0L st Bottom 0L in A for B holds
B c= A implies FinJoin B in A
proof
let A be ClosedSubset of 0L;
defpred X[Element of Fin the carrier of 0L] means $1 c= A implies FinJoin
$1 in A;
A1: for B1 being Element of Fin the carrier of 0L for p being Element of
0L st X[B1] holds X[B1 \/ {.p.}]
proof
let B1 be Element of Fin the carrier of 0L;
let p be Element of 0L;
assume
A2: B1 c=A implies FinJoin B1 in A;
assume
A3: B1 \/ {p} c=A;
then {p} c= A by XBOOLE_1:11;
then p in A by ZFMISC_1:31;
then FinJoin B1 "\/" p in A by A2,A3,LATTICES:def 25,XBOOLE_1:11;
hence thesis by Th14;
end;
assume Bottom 0L in A;
then
A4: X[{}.the carrier of 0L] by Lm1;
thus for B being Element of Fin the carrier of 0L holds X[B] from SETWISEO:
sch 4(A4,A1);
end;
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 Th18:
for f being Homomorphism of 1L,L2 st f is onto holds
L2 is upper-bounded & f preserves_top
proof
let f be Homomorphism of 1L,L2;
set r = f.(Top 1L);
assume
A1: f is onto;
A2: now
let a2 be Element of L2;
consider a1 be Element of 1L such that
A3: f.a1 = a2 by A1,Th6;
thus r"\/"a2 = f.(Top 1L "\/" a1) by A3,D1
.= r;
hence a2"\/"r = r;
end;
thus L2 is upper-bounded
by A2;
then Top L2=r by A2,LATTICES:def 17;
hence thesis;
end;
Lm2: for f being Function of the carrier of 1L, the carrier of 1L holds
FinMeet ({}.the carrier of 1L,f) = Top 1L
proof
let f be Function of the carrier of 1L, the carrier of 1L;
set M=the L_meet of 1L;
thus FinMeet ({}.the carrier of 1L,f) = M $$ ({}.the carrier of 1L,f) by
LATTICE2:def 4
.= the_unity_wrt M by SETWISEO:31
.= Top 1L by LATTICE2:57;
end;
theorem
FinMeet {}.the carrier of 1L = Top 1L by Lm2;
reserve f,g for UnOp of the carrier of 1L;
theorem Th20:
FinMeet(B \/ {.b.},f) = FinMeet (B,f) "/\" f.b
proof
set M= the L_meet of 1L;
thus FinMeet (B \/ {.b.},f) = M $$ (B \/ {.b.},f) by LATTICE2:def 4
.= M $$ (B,f) "/\" f.b by SETWISEO:32
.= FinMeet (B,f) "/\" f.b by LATTICE2:def 4;
end;
theorem Th21:
FinMeet(B \/ {.b.}) = FinMeet B "/\" b
proof
thus FinMeet(B \/ {.b.}) =FinMeet (B,id 1L) "/\" (id 1L).b by Th20
.= FinMeet B "/\" b by FUNCT_1:18;
end;
theorem Th22:
FinMeet(f.:B,g) = FinMeet(B,g*f)
proof
set M= the L_meet of 1L;
thus FinMeet(f.:B,g) = M$$(f.:B,g) by LATTICE2:def 4
.= M$$(B,g*f) by SETWISEO:35
.= FinMeet(B,g*f)by LATTICE2:def 4;
end;
theorem Th23:
FinMeet B1 "/\" FinMeet B2 = FinMeet (B1 \/ B2)
proof
set M = the L_meet of 1L;
thus FinMeet (B1 \/ B2) = M $$ (B1 \/ B2,id 1L) by LATTICE2:def 4
.= M $$ (B1,id 1L) "/\" M $$ (B2,id 1L) by SETWISEO:33
.= FinMeet B1 "/\" M $$ (B2,id 1L) by LATTICE2:def 4
.=FinMeet B1 "/\" FinMeet B2 by LATTICE2:def 4;
end;
theorem Th24:
for F being ClosedSubset of 1L st Top 1L in F for B holds B c= F
implies FinMeet B in F
proof
let F be ClosedSubset of 1L;
defpred X[Element of Fin the carrier of 1L] means $1 c= F implies FinMeet
$1 in F;
A1: for B1 being Element of Fin the carrier of 1L for p being Element of
1L st X[B1] holds X[B1 \/ {.p.}]
proof
let B1 be Element of Fin the carrier of 1L;
let p be Element of 1L;
assume
A2: B1 c=F implies FinMeet B1 in F;
assume
A3: B1 \/ {p} c=F;
then {p} c= F by XBOOLE_1:11;
then p in F by ZFMISC_1:31;
then FinMeet B1 "/\" p in F by A2,A3,LATTICES:def 24,XBOOLE_1:11;
hence thesis by Th21;
end;
assume Top 1L in F;
then
A4: X[{}.the carrier of 1L] by Lm2;
thus for B being Element of Fin the carrier of 1L holds X[B] from SETWISEO:
sch 4(A4,A1);
end;
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;
Lm3: (the L_join of DL).((the L_meet of DL) $$ (B,f),p) = (the L_meet of DL)
$$ (B,(the L_join of DL) [:] (f,p))
proof
set J = the L_join of DL;
set M = the L_meet of DL;
now
per cases;
suppose
B<> {};
hence thesis by LATTICE2:21,SETWISEO:28;
end;
suppose
A1: B = {};
A2: now
let f;
thus M $$ (B,f) = FinMeet({}.the carrier of DL,f) by A1,LATTICE2:def 4
.=Top DL by Lm2;
end;
hence J.(M $$ (B,f),p) = Top DL "\/" p .= Top DL
.= M $$ (B,J [:] (f,p)) by A2;
end;
end;
hence thesis;
end;
theorem Th25:
FinMeet B "\/" p = FinMeet (((the L_join of DL)[:](id DL,p)).:B)
proof
set J = the L_join of DL;
set M = the L_meet of DL;
thus FinMeet B "\/" p = J.(M $$ (B,id DL),p) by LATTICE2:def 4
.= M $$ (B,J [:] (id DL,p)) by Lm3
.=FinMeet(B,J [:] (id DL,p)) by LATTICE2:def 4
.= FinMeet (B,(id DL)*(J [:] (id DL,p))) by FUNCT_2:17
.= FinMeet (((the L_join of DL)[:](id DL,p)).: B) by Th22;
end;
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 Th26:
f.i "/\" f.(i => j) [= f.j
proof
i "/\" (i => j) [= j by FILTER_0:def 7;
then f.(i "/\" (i => j)) [= f.j by Th4;
hence thesis by D2;
end;
theorem Th27:
f is one-to-one implies (f.i "/\" f.k [= f.j implies f.k [= f.(i => j))
proof
assume
A1: f is one-to-one;
hereby
assume f.i "/\" f.k [= f.j;
then f.(i "/\" k) [= f.j by D2;
then i "/\" k [= j by A1,Th5;
then k [= (i => j) by FILTER_0:def 7;
hence f.k [= f.(i => j) by Th4;
end;
end;
theorem
f is bijective implies CL is implicative & f preserves_implication
proof
assume
A1: f is bijective;
thus CL is implicative
proof
let p,q be Element of CL;
consider i such that
A2: f.i=p by A1,Th6;
consider j such that
A3: f.j=q by A1,Th6;
take r = f.(i => j);
thus p "/\" r [= q by A2,A3,Th26;
hereby
let r1 be Element of CL;
assume
A4: p "/\" r1 [= q;
ex k st f.k = r1 by A1,Th6;
hence r1 [= r by A1,A2,A3,A4,Th27;
end;
end;
then reconsider CL as implicative Lattice;
reconsider f as Homomorphism of IL,CL;
now
let i,j;
A5: now
let r1 be Element of CL;
assume
A6: (f.i) "/\" r1 [= (f.j);
ex k st f.k=r1 by A1,Th6;
hence r1 [= f.(i => j) by A1,A6,Th27;
end;
(f.i) "/\" f.(i => j) [= (f.j) by Th26;
hence (f.i) => (f.j) = f.(i => j) by A5,FILTER_0:def 7;
end;
hence thesis;
end;
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 Th29:
(Top BL)` = Bottom BL
proof
set a=Bottom BL;
thus (Top BL)` = (a "\/" a`)` by LATTICES:21
.= a` "/\"a``
.= Bottom BL;
end;
theorem Th30:
(Bottom BL)` = Top BL
proof
set a = Top BL;
thus (Bottom BL)` = (a "/\" a`)` by LATTICES:20
.= a` "\/"a``
.= Top BL;
end;
theorem
f is onto implies CL is Boolean & f preserves_complement
proof
assume
A1: f is onto;
then
A2: f preserves_top by Th18;
thus CL is bounded complemented;
thus CL is distributive by A1,Th11;
then reconsider CL as Boolean Lattice;
A3: f preserves_bottom by A1,Th12;
reconsider f as Homomorphism of BL,CL;
now
let a1;
A4: f.(a1`)"/\"f.a1 = f.(a1` "/\" a1) by D2
.=f.(Bottom BL) by LATTICES:20
.= Bottom CL by A3;
A5: f.(a1`)"\/"f.a1 = f.a1"\/"f.(a1`) & f.(a1`)"/\"f.a1 = f.a1"/\"f.(a1`);
f.(a1`)"\/"f.a1 =f.(a1` "\/" a1) by D1
.=f.(Top BL) by LATTICES:21
.= Top CL by A2;
then f.(a1`) is_a_complement_of f.a1 by A4,A5;
hence (f.a1)` = f.(a1`) by LATTICES:def 21;
end;
hence thesis;
end;
definition
let BL;
mode Field of BL -> non empty Subset of BL means
:Def9:
a in it & b in it implies a "/\" b in it & a` in it;
existence
proof
the carrier of BL c= the carrier of BL;
then reconsider F=the carrier of BL as non empty Subset of BL;
take F;
thus thesis;
end;
end;
reserve F,H for Field of BL;
theorem Th32:
a in F & b in F implies a "\/" b in F
proof
assume a in F & b in F;
then a` in F & b` in F by Def9;
then a` "/\" b` in F by Def9;
then ( a"\/"b )` in F by LATTICES:24;
then ( a"\/"b )`` in F by Def9;
hence thesis;
end;
theorem Th33:
a in F & b in F implies a => b in F
proof
assume that
A1: a in F and
A2: b in F;
a` in F by A1,Def9;
then a` "\/" b in F by A2,Th32;
hence thesis by FILTER_0:42;
end;
theorem Th34:
the carrier of BL is Field of BL
proof
the carrier of BL c= the carrier of BL;
then reconsider F=the carrier of BL as non empty Subset of BL;
a in F & b in F implies a "/\" b in F & a` in F;
hence thesis by Def9;
end;
theorem Th35:
F is ClosedSubset of BL
proof
A1: for a,b st a in F & b in F holds a "/\" b in F by Def9;
for a,b st a in F & b in F holds a "\/" b in F by Th32;
hence thesis by A1,LATTICES:def 24,def 25;
end;
definition
let BL,A;
func field_by A -> Field of BL means
:Def10:
A c= it & for F st A c= F holds it c= F;
existence
proof
set x = the Element of A;
defpred X[set] means $1 is Field of BL & A c= $1;
consider X such that
A1: Z in X iff Z in bool the carrier of BL & X[Z] from XFAMILY:sch 1;
reconsider x as Element of BL;
A2: the carrier of BL is Field of BL by Th34;
then
A3: X <> {} by A1;
now
let Z;
assume Z in X;
then A c= Z by A1;
hence x in Z;
end;
then reconsider F1 = meet X as non empty set by A3,SETFAM_1:def 1;
A4: the carrier of BL in X by A1,A2;
F1 c= the carrier of BL
by A4,SETFAM_1:def 1;
then reconsider F1 as non empty Subset of BL;
F1 is Field of BL
proof
let a,b;
assume that
A5: a in F1 and
A6: b in F1;
A7: for Z st Z in X holds a "/\" b in Z
proof
let Z;
assume
A8: Z in X;
then
A9: b in Z by A6,SETFAM_1:def 1;
Z is Field of BL & a in Z by A1,A5,A8,SETFAM_1:def 1;
hence thesis by A9,Def9;
end;
for Z st Z in X holds a` in Z
proof
let Z;
assume Z in X;
then Z is Field of BL & a in Z by A1,A5,SETFAM_1:def 1;
hence thesis by Def9;
end;
hence thesis by A3,A7,SETFAM_1:def 1;
end;
then reconsider F = F1 as Field of BL;
take F;
for Z st Z in X holds A c= Z by A1;
hence A c= F by A4,SETFAM_1:5;
let H;
assume A c= H;
then H in X by A1;
hence thesis by SETFAM_1:3;
end;
uniqueness
proof
let F1,F2 be Field of BL;
assume ( A c= F1 & for F st A c= F holds F1 c= F )&( A c= F2 & for F st
A c= F holds F2 c= F );
hence F1 c= F2 & F2 c= F1;
end;
end;
definition
let BL,A;
func SetImp A -> Subset of BL equals
{ a => b : a in A & b in A};
coherence
proof
set B={ a => b : a in A & b in A};
B c= the carrier of BL
proof
let x be object;
assume x in B;
then ex p,q st x = p => q & p in A & q in A;
hence thesis;
end;
hence thesis;
end;
end;
registration
let BL,A;
cluster SetImp A -> non empty;
coherence
proof
set x = the Element of A;
set B={ a => b : a in A & b in A};
reconsider x as Element of BL;
x => x in B;
then reconsider B as non empty set;
B = SetImp A;
hence thesis;
end;
end;
theorem
x in SetImp A iff ex p,q st x = p => q & p in A & q in A;
theorem Th37:
c in SetImp A iff ex p,q st c = p` "\/" q & p in A & q in A
proof
hereby
assume c in SetImp A;
then consider p,q such that
A1: c = p => q & p in A & q in A;
take p,q;
thus c = p` "\/" q & p in A & q in A by A1,FILTER_0:42;
end;
given p,q such that
A2: c = p` "\/" q and
A3: p in A & q in A;
c = p => q by A2,FILTER_0:42;
hence thesis by A3;
end;
definition
let BL;
deffunc U(Element of BL) = $1`;
func comp BL -> Function of the carrier of BL, the carrier of BL means
:
Def12: it.a = a`;
existence
proof
consider f being Function of the carrier of BL,the carrier of BL such that
A1: for a holds f.a= U(a) from FUNCT_2:sch 4;
take f;
thus thesis by A1;
end;
uniqueness
proof
thus for f1,f2 being Function of the carrier of BL,the carrier of BL st (
for x being Element of BL holds f1.x = U(x)) & (for x being Element of BL holds
f2.x = U(x)) holds f1 = f2 from BINOP_2:sch 1;
end;
end;
theorem Th38:
FinJoin(B \/ {.b.},comp BL) = FinJoin (B,comp BL) "\/" b`
proof
thus FinJoin(B \/ {.b.},comp BL) = FinJoin(B,comp BL) "\/" (comp BL).b by
Th13
.= FinJoin (B,comp BL) "\/" b` by Def12;
end;
theorem
(FinJoin B)` = FinMeet (B,comp BL)
proof
set M= the L_meet of BL;
set J= the L_join of BL;
A1: for a,b being Element of BL holds (comp BL).(J.(a,b))= M.((comp BL).a,(
comp BL).b)
proof
let a,b be Element of BL;
thus (comp BL).(J.(a,b))=(a"\/"b)` by Def12
.=a`"/\"b` by LATTICES:24
.= M.((comp BL).a,b`) by Def12
.= M.((comp BL).a,(comp BL).b) by Def12;
end;
A2: (comp BL).(the_unity_wrt J)= (the_unity_wrt J)` by Def12
.=(Bottom BL )` by LATTICE2:52
.=Top BL by Th30
.= the_unity_wrt M by LATTICE2:57;
thus (FinJoin B)`= (J$$(B,id BL))` by LATTICE2:def 3
.= (comp BL).(J$$(B,id BL)) by Def12
.= M$$(B,(comp BL)*(id BL)) by A2,A1,SETWISEO:36
.= M$$(B, comp BL) by FUNCT_2:17
.= FinMeet(B, comp BL) by LATTICE2:def 4;
end;
theorem
FinMeet(B \/ {.b.},comp BL) = FinMeet (B,comp BL) "/\" b`
proof
thus FinMeet(B \/ {.b.},comp BL) =FinMeet (B,comp BL) "/\" (comp BL).b by
Th20
.=FinMeet (B,comp BL) "/\" b` by Def12;
end;
theorem Th41:
(FinMeet B)` = FinJoin (B,comp BL)
proof
set M= the L_meet of BL;
set J= the L_join of BL;
A1: for a,b being Element of BL holds (comp BL).(M.(a,b))= J.((comp BL).a,(
comp BL).b)
proof
let a,b be Element of BL;
thus (comp BL).(M.(a,b))=(a"/\"b)` by Def12
.=a`"\/"b` by LATTICES:23
.= J.((comp BL).a,b`) by Def12
.= J.((comp BL).a,(comp BL).b) by Def12;
end;
A2: (comp BL).(the_unity_wrt M)= (the_unity_wrt M)` by Def12
.=(Top BL )` by LATTICE2:57
.=Bottom BL by Th29
.= the_unity_wrt J by LATTICE2:52;
thus (FinMeet B)`= (M$$(B,id BL))` by LATTICE2:def 4
.= (comp BL).(M$$(B,id BL)) by Def12
.= J$$(B,(comp BL)*(id BL)) by A2,A1,SETWISEO:36
.= J$$(B, comp BL) by FUNCT_2:17
.= FinJoin(B, comp BL) by LATTICE2:def 3;
end;
theorem Th42:
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
proof
let AF be non empty ClosedSubset of BL such that
A1: Bottom BL in AF and
A2: Top BL in AF;
set C={ FinJoin A1 "\/" FinJoin(A2,comp BL): A1 c= AF & A2 c= AF};
A3: C c= SetImp AF
proof
let x be object;
assume x in C;
then consider A1,A2 such that
A4: x = FinJoin A1 "\/" FinJoin(A2,comp BL) and
A5: A1 c= AF & A2 c= AF;
consider p,q such that
A6: p = FinMeet A2 & q = FinJoin A1;
A7: x = p` "\/" q by A4,A6,Th41;
p in AF & q in AF by A1,A2,A5,A6,Th17,Th24;
hence thesis by A7,Th37;
end;
defpred X[Element of Fin the carrier of BL] means $1 c= SetImp AF implies
ex B0 st B0 c= C & FinJoin($1,comp BL) = FinMeet B0;
let B;
assume
A8: B c= SetImp AF;
A9: for B9 being Element of Fin the carrier of BL, b being Element of BL
st X[B9] holds X[B9 \/ {.b.}]
proof
set J = the L_join of BL;
let B9 be Element of Fin the carrier of BL, b be Element of BL;
assume
A10: B9 c= SetImp AF implies ex B1 st B1 c= C & FinJoin(B9,comp BL) =
FinMeet B1;
assume
A11: B9 \/ {b} c= SetImp AF;
then consider B1 such that
A12: B1 c= C and
A13: FinJoin(B9,comp BL) = FinMeet B1 by A10,ZFMISC_1:137;
b in SetImp AF by A11,ZFMISC_1:137;
then consider p,q such that
A14: b = p` "\/" q and
A15: p in AF and
A16: q in AF by Th37;
A17: for x,b holds x in (J[:](id BL,b)).:B1 implies ex a st a in B1 & x =
a "\/" b
proof
let x,b;
assume
A18: x in (J[:](id BL,b)).:B1;
(J[:](id BL,b)).:B1 c= the carrier of BL by FUNCT_2:36;
then reconsider x as Element of BL by A18;
consider a such that
A19: a in B1 and
A20: x = (J[:](id BL,b)).a by A18,FUNCT_2:65;
x = J.(id BL.a,b) by A20,FUNCOP_1:48
.= a "\/" b by FUNCT_1:18;
hence thesis by A19;
end;
A21: (J[:](id BL,p)).:B1 c= C
proof
let x be object;
assume x in (J[:](id BL,p)).:B1;
then consider a such that
A22: a in B1 and
A23: x = a "\/" p by A17;
a in C by A12,A22;
then consider A1,A2 such that
A24: a = FinJoin A1 "\/" FinJoin(A2,comp BL) and
A25: A1 c= AF & A2 c= AF;
ex A19,A29 being Element of Fin the carrier of BL st x = FinJoin
A19 "\/" FinJoin (A29,comp BL) & A19 c= AF & A29 c= AF
proof
take A19=A1 \/ {.p.};
take A29=A2;
x = (FinJoin A1 "\/" p) "\/" FinJoin(A2,comp BL) by A23,A24,
LATTICES:def 5
.= FinJoin(A19) "\/" FinJoin(A29,comp BL) by Th14;
hence thesis by A15,A25,ZFMISC_1:137;
end;
hence thesis;
end;
A26: (J[:](id BL,q`)).:B1 c= C
proof
let x be object;
assume x in (J[:](id BL,q`)).:B1;
then consider a such that
A27: a in B1 and
A28: x = a "\/" q` by A17;
a in C by A12,A27;
then consider A1,A2 such that
A29: a = FinJoin A1 "\/" FinJoin(A2,comp BL) and
A30: A1 c= AF & A2 c= AF;
ex A19,A29 being Element of Fin the carrier of BL st x = FinJoin
A19 "\/" FinJoin (A29,comp BL) & A19 c= AF & A29 c= AF
proof
take A19=A1;
take A29=A2 \/ {.q.};
x = FinJoin A1 "\/" (FinJoin(A2,comp BL) "\/" q`) by A28,A29,
LATTICES:def 5
.= FinJoin(A19) "\/" FinJoin(A29,comp BL) by Th38;
hence thesis by A16,A30,ZFMISC_1:137;
end;
hence thesis;
end;
take (J[:](id BL,p)).:B1 \/ (J[:](id BL,q`)).:B1;
b` = p`` "/\" q` by A14,LATTICES:24
.= p "/\" q`;
then FinJoin(B9 \/ {.b.} ,comp BL) = FinMeet B1 "\/" (p "/\" q`) by A13
,Th38
.= (FinMeet B1 "\/" p) "/\" (FinMeet B1 "\/" q`) by LATTICES:11
.= FinMeet((J[:](id BL,p)).:B1) "/\" (FinMeet B1 "\/" q`) by Th25
.= FinMeet((J[:](id BL,p)).:B1) "/\" FinMeet ((J[:] (id BL,q`)).:B1)
by Th25
.= FinMeet ((J[:](id BL,p)).:B1 \/ (J[:](id BL,q`)).:B1) by Th23;
hence thesis by A21,A26,XBOOLE_1:8;
end;
A31: X[{}.the carrier of BL]
proof
assume {}.the carrier of BL c= SetImp AF;
take B0={.Bottom BL.};
A32: B0 c= C
proof
let x be object;
assume x in B0;
then
A33: x = Bottom BL by TARSKI:def 1;
ex A1,A2 st x = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF
proof
take A1={.Bottom BL.};
take A2={.Top BL.};
thus x = Bottom BL "\/" Bottom BL by A33
.= Bottom BL "\/" (Top BL)` by Th29
.=FinJoin A1 "\/" (Top BL)` by Th9
.=FinJoin A1 "\/" (FinMeet A2)` by Th10
.=FinJoin A1 "\/" FinJoin (A2,comp BL) by Th41;
thus A1 c= AF by A1,ZFMISC_1:31;
thus thesis by A2,ZFMISC_1:31;
end;
hence thesis;
end;
FinJoin ({}.the carrier of BL,comp BL)= Bottom BL by Lm1
.=FinMeet {.Bottom BL.} by Th10;
hence thesis by A32;
end;
for B being Element of Fin the carrier of BL holds X[B] from SETWISEO
:sch 4(A31,A9);
then ex B1 st B1 c= C & FinJoin(B,comp BL) = FinMeet B1 by A8;
hence thesis by A3,XBOOLE_1:1;
end;
theorem
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
proof
let AF be non empty ClosedSubset of BL such that
A1: Bottom BL in AF and
A2: Top BL in AF;
set A1= { FinMeet B :B c= SetImp AF };
A3: AF c= A1
proof
let x be object;
assume
A4: x in AF;
then reconsider b=x as Element of BL;
reconsider B = {.b.} as Element of Fin the carrier of BL;
b = Bottom BL "\/" b
.= (Top BL)` "\/" b by Th29;
then b in SetImp AF by A2,A4,Th37;
then
A5: B c= SetImp AF by ZFMISC_1:31;
x = FinMeet B by Th10;
hence thesis by A5;
end;
A1 c= the carrier of BL
proof
let x be object;
assume x in A1;
then ex B st x = FinMeet B & B c= SetImp AF;
hence thesis;
end;
then reconsider A1 as non empty Subset of BL by A3;
A6: now
let F;
assume
A7: AF c= F;
thus A1 c= F
proof
reconsider F1=F as ClosedSubset of BL by Th35;
let x be object;
assume x in A1;
then consider B such that
A8: x=FinMeet B and
A9: B c= SetImp AF;
SetImp AF c= F
proof
let y be object;
assume y in SetImp AF;
then ex p,q st y = p => q & p in AF & q in AF;
hence thesis by A7,Th33;
end;
then B c= F1 by A9;
hence thesis by A2,A7,A8,Th24;
end;
end;
A1 is Field of BL
proof
let p,q;
assume that
A10: p in A1 and
A11: q in A1;
thus p "/\" q in A1
proof
consider B2 such that
A12: q=FinMeet B2 & B2 c= SetImp AF by A11;
consider B1 such that
A13: p=FinMeet B1 & B1 c= SetImp AF by A10;
consider B0 such that
A14: B0=B1 \/ B2;
B0 c= SetImp AF & p "/\" q = FinMeet B0 by A13,A12,A14,Th23,XBOOLE_1:8;
hence thesis;
end;
thus p` in A1
proof
consider B such that
A15: p=FinMeet B and
A16: B c= SetImp AF by A10;
p` = FinJoin ( B,comp BL) by A15,Th41;
then ex B0 st B0 c= SetImp AF & p` = FinMeet B0 by A1,A2,A16,Th42;
hence thesis;
end;
end;
hence thesis by A3,A6,Def10;
end;