:: Finite Join and Finite Meet, and Dual Lattices
:: by Andrzej Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990-2021 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, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4, TARSKI, FINSUB_1,
BINOP_1, LATTICES, EQREL_1, STRUCT_0, PBOOLE, SETWISEO, FUNCOP_1,
FILTER_0, FINSET_1, XXREAL_2, LATTICE2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4,
PARTFUN1, FUNCOP_1, BINOP_1, FINSET_1, STRUCT_0, LATTICES, FINSUB_1,
SETWISEO, FILTER_0;
constructors BINOP_1, FUNCOP_1, FUNCT_4, SETWISEO, GROUP_1, FILTER_0,
RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES,
FILTER_0;
requirements SUBSET, BOOLE;
definitions LATTICES, BINOP_1, SETWISEO, FILTER_0;
equalities LATTICES;
expansions LATTICES, BINOP_1, SETWISEO;
theorems LATTICES, BINOP_1, SETWISEO, FUNCOP_1, FUNCT_4, SETWOP_2, FINSET_1,
FINSUB_1, FUNCT_2, FUNCT_1, FILTER_0, GRFUNC_1, RELAT_1, RLSUB_2,
XBOOLE_1;
schemes FRAENKEL;
begin :: Auxiliary theorems
reserve A for set,
C for non empty set,
B for Subset of A,
x for Element of A,
f,g for Function of A,C;
theorem Th1:
dom (g|B) = B
proof
thus dom(g|B) = dom g /\ B by RELAT_1:61
.= A /\ B by FUNCT_2:def 1
.= B by XBOOLE_1:28;
end;
theorem Th2:
f|B = g|B iff for x st x in B holds g.x = f.x
proof
thus f|B = g|B implies for x st x in B holds g.x = f.x
proof
assume
A1: f|B = g|B;
let x;
assume
A2: x in B;
hence g.x = (g|B).x by FUNCT_1:49
.= f.x by A1,A2,FUNCT_1:49;
end;
reconsider f9=f|B, g9=g|B as Function of B,C by FUNCT_2:32;
assume
A3: for x st x in B holds g.x = f.x;
A4: now
let x be object;
assume
A5: x in B;
hence f9.x = f.x by FUNCT_1:49
.= g.x by A3,A5
.= g9.x by A5,FUNCT_1:49;
end;
thus f|B = f9|B
.= g9|B by A4,FUNCT_2:12
.= g|B;
end;
theorem Th3:
for B being set holds f +* g|B is Function of A,C
proof
let B be set;
A1: dom f = A & dom g = A by FUNCT_2:def 1;
dom (f +* g|B) = dom f \/ dom (g|B) by FUNCT_4:def 1
.= dom f \/ dom g /\ B by RELAT_1:61
.= A by A1,XBOOLE_1:22;
hence thesis by FUNCT_2:67;
end;
theorem Th4:
g|B +* f = f
proof
dom (g|B) = B & dom f = A by Th1,FUNCT_2:def 1;
hence thesis by FUNCT_4:19;
end;
theorem Th5:
for f,g being Function holds g c= f implies f +* g = f
proof
let f,g be Function;
assume
A1: g c= f;
then dom g c= dom f by GRFUNC_1:2;
then
A2: dom f = dom f \/ dom g by XBOOLE_1:12;
for x be object st x in dom f holds (x in dom g implies f.x = g.x) & (not x
in dom g implies f.x = f.x) by A1,GRFUNC_1:2;
hence thesis by A2,FUNCT_4:def 1;
end;
theorem
f +* f|B = f by Th5,RELAT_1:59;
theorem Th7:
(for x st x in B holds g.x = f.x) implies f +* g|B = f
proof
assume x in B implies g.x = f.x;
then g|B = f|B by Th2;
hence thesis by Th5,RELAT_1:59;
end;
reserve B for Element of Fin A;
theorem
g|B +* f = f
proof
reconsider C = B as Subset of A by FINSUB_1:16;
g|C +* f = f by Th4;
hence thesis;
end;
theorem Th9:
dom (g|B) = B
proof
reconsider C = B as Subset of A by FINSUB_1:16;
dom (g|C) = C by Th1;
hence thesis;
end;
theorem Th10:
(for x st x in B holds g.x = f.x) implies f +* g|B = f
proof
reconsider C = B as Subset of A by FINSUB_1:16;
(for x st x in C holds g.x = f.x) implies f +* g|C = f by Th7;
hence thesis;
end;
definition
let D be non empty set;
let o,o9 be BinOp of D;
pred o absorbs o9 means
for x,y being Element of D holds o.(x,o9.(x,y )) = x;
end;
notation
let D be non empty set;
let o,o9 be BinOp of D;
antonym o doesn't_absorb o9 for o absorbs o9;
end;
:: Dual Lattice structures
reserve L for non empty LattStr,
a,b,c for Element of L;
theorem Th11:
the L_join of L is commutative associative & the L_meet of L is
commutative associative & the L_join of L absorbs the L_meet of L & the L_meet
of L absorbs the L_join of L implies L is Lattice-like
proof
assume that
A1: the L_join of L is commutative and
A2: the L_join of L is associative and
A3: the L_meet of L is commutative and
A4: the L_meet of L is associative and
A5: the L_join of L absorbs the L_meet of L and
A6: the L_meet of L absorbs the L_join of L;
thus a"\/"b = b"\/"a by A1;
thus a"\/"(b"\/"c) = (a"\/"b)"\/"c by A2;
thus (a"/\"b)"\/"b = b
proof
thus (a"/\"b)"\/"b = b "\/" (a "/\" b) by A1
.= b "\/" (b "/\" a) by A3
.= b by A5;
end;
thus a"/\"b = b"/\"a by A3;
thus a"/\"(b"/\"c) = (a"/\"b)"/\"c by A4;
let a,b;
thus thesis by A6;
end;
definition
let L be LattStr;
func L.: -> strict LattStr equals
LattStr(#the carrier of L, the L_meet of L
, the L_join of L#);
correctness;
end;
registration
let L be non empty LattStr;
cluster L.: -> non empty;
coherence;
end;
theorem
the carrier of L = the carrier of L.: & the L_join of L = the L_meet
of L.: & the L_meet of L = the L_join of L.:;
theorem
for L being strict non empty LattStr holds L .: .: = L;
:: General Lattices
reserve L for Lattice;
reserve a,b,c,u,v for Element of L;
theorem Th14:
(for v holds u "\/" v = v) implies u = Bottom L
proof
assume
A1: u "\/" v = v;
now
let v;
v "\/" u = v by A1;
then u [= v;
hence v "/\" u = u by LATTICES:4;
end;
hence thesis by RLSUB_2:64;
end;
theorem Th15:
(for v holds (the L_join of L).(u,v) = v) implies u = Bottom L
proof
assume for v holds (the L_join of L).(u,v) = v;
then for v holds u "\/" v = v;
hence thesis by Th14;
end;
theorem Th16:
(for v holds u "/\" v = v) implies u = Top L
proof
assume
A1: u "/\" v = v;
now
let v;
v "/\" u = v by A1;
then v [= u by LATTICES:4;
hence u = v "\/" u;
end;
hence thesis by RLSUB_2:65;
end;
theorem Th17:
(for v holds (the L_meet of L).(u,v) = v) implies u = Top L
proof
assume for v holds (the L_meet of L).(u,v) = v;
then for v holds u "/\" v = v;
hence thesis by Th16;
end;
registration
let L;
cluster the L_join of L -> idempotent;
coherence
proof
let a;
thus (the L_join of L).(a,a) = a "\/" a .= a;
end;
end;
registration
let L be join-commutative non empty \/-SemiLattStr;
cluster the L_join of L -> commutative;
coherence
proof
let a,b be Element of L;
thus (the L_join of L).(a,b) = b "\/" a by LATTICES:def 1
.= (the L_join of L).(b,a);
end;
end;
theorem Th18:
the L_join of L is having_a_unity implies Bottom L =
the_unity_wrt the L_join of L
proof
set J = the L_join of L;
given u such that
A1: u is_a_unity_wrt J;
(the L_join of L).(u,v) = v by A1,BINOP_1:4;
then u = Bottom L by Th15;
hence thesis by A1,BINOP_1:def 8;
end;
registration
let L be join-associative non empty \/-SemiLattStr;
cluster the L_join of L -> associative;
coherence
proof
let a,b,c be Element of L;
thus (the L_join of L).(a,(the L_join of L).(b,c)) = a "\/" (b "\/" c)
.= (a "\/" b) "\/" c by LATTICES:def 5
.= (the L_join of L).((the L_join of L).(a,b),c);
end;
end;
registration
let L;
cluster the L_meet of L -> idempotent;
coherence
proof
let a;
thus (the L_meet of L).(a,a) = a "/\" a .= a;
end;
end;
registration
let L be meet-commutative non empty /\-SemiLattStr;
cluster the L_meet of L -> commutative;
coherence
proof
let a,b be Element of L;
thus (the L_meet of L).(a,b) = b "/\" a by LATTICES:def 2
.= (the L_meet of L).(b,a);
end;
end;
registration
let L be meet-associative non empty /\-SemiLattStr;
cluster the L_meet of L -> associative;
coherence
proof
let a,b,c be Element of L;
thus (the L_meet of L).(a,(the L_meet of L).(b,c)) = a "/\" (b "/\" c)
.= (a "/\" b) "/\" c by LATTICES:def 7
.= (the L_meet of L).((the L_meet of L).(a,b),c);
end;
end;
theorem Th19:
the L_meet of L is having_a_unity implies Top L = the_unity_wrt
the L_meet of L
proof
set J = the L_meet of L;
given u such that
A1: u is_a_unity_wrt J;
(the L_meet of L).(u,v) = v by A1,BINOP_1:4;
then u = Top L by Th17;
hence thesis by A1,BINOP_1:def 8;
end;
theorem Th20:
the L_join of L is_distributive_wrt the L_join of L
proof
now
let a,b,c;
thus (the L_join of L).(a,(the L_join of L).(b,c)) = a "\/" (b "\/" c)
.= a "\/" b "\/" c by LATTICES:def 5
.= a "\/" a "\/" b "\/" c
.= (a "\/" b) "\/" a "\/" c by LATTICES:def 5
.= (a "\/" b) "\/" (a "\/" c) by LATTICES:def 5
.= (the L_join of L).((the L_join of L).(a,b),(the L_join of L).(a,c));
end;
hence thesis by BINOP_1:12;
end;
theorem
L is D_Lattice implies the L_join of L is_distributive_wrt the L_meet of L
proof
assume
A1: L is D_Lattice;
now
let a,b,c;
thus (the L_join of L).(a,(the L_meet of L).(b,c)) = a "\/" (b "/\" c)
.= (a "\/" b) "/\" (a "\/" c) by A1,LATTICES:11
.= (the L_meet of L).((the L_join of L).(a,b),(the L_join of L).(a,c));
end;
hence thesis by BINOP_1:12;
end;
theorem Th22:
the L_join of L is_distributive_wrt the L_meet of L implies L is distributive
proof
assume
A1: the L_join of L is_distributive_wrt the L_meet of L;
then
A2: for a,b,c holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)by BINOP_1:12
;
let a,b,c;
thus a"/\"(b"\/"c) = a"/\"(c"\/"a)"/\"(c"\/"b) by LATTICES:def 9
.= a"/\"((c"\/"a)"/\"(c"\/"b)) by LATTICES:def 7
.= a"/\"((a"/\"b)"\/"c) by A2
.= ((a"/\"b)"\/"a)"/\"((a"/\"b)"\/"c) by LATTICES:def 8
.= (a"/\"b)"\/"(a"/\"c) by A1,BINOP_1:12;
end;
theorem Th23:
L is D_Lattice implies the L_meet of L is_distributive_wrt the L_join of L
proof
assume
A1: L is D_Lattice;
now
let a,b,c;
thus (the L_meet of L).(a,(the L_join of L).(b,c)) = a "/\" (b "\/" c)
.= (a "/\" b) "\/" (a "/\" c) by A1,LATTICES:def 11
.= (the L_join of L).((the L_meet of L).(a,b),(the L_meet of L).(a,c));
end;
hence thesis by BINOP_1:12;
end;
theorem
the L_meet of L is_distributive_wrt the L_join of L implies L is distributive
by BINOP_1:12;
theorem Th25:
the L_meet of L is_distributive_wrt the L_meet of L
proof
now
let a,b,c;
thus (the L_meet of L).(a,(the L_meet of L).(b,c)) = a "/\" (b "/\" c)
.= a "/\" b "/\" c by LATTICES:def 7
.= a "/\" a "/\" b "/\" c
.= (a "/\" b) "/\" a "/\" c by LATTICES:def 7
.= (a "/\" b) "/\" (a "/\" c) by LATTICES:def 7
.= (the L_meet of L).((the L_meet of L).(a,b),(the L_meet of L).(a,c));
end;
hence thesis by BINOP_1:12;
end;
theorem Th26:
the L_join of L absorbs the L_meet of L
proof
let x,y be Element of L;
thus (the L_join of L).(x,(the L_meet of L).(x,y)) = x "\/"(x "/\" y)
.= x by LATTICES:def 8;
end;
theorem Th27:
the L_meet of L absorbs the L_join of L
proof
let x,y be Element of L;
thus (the L_meet of L).(x,(the L_join of L).(x,y)) = x "/\"(x "\/" y)
.= x by LATTICES:def 9;
end;
definition
let A be non empty set, L be Lattice;
let B be Element of Fin A;
let f be Function of A, the carrier of L;
func FinJoin(B, f) -> Element of L equals
(the L_join of L)$$(B,f);
correctness;
func FinMeet(B, f) -> Element of L equals
(the L_meet of L)$$(B,f);
correctness;
end;
reserve A for non empty set,
x for Element of A,
B for Element of Fin A,
f,g for Function of A, the carrier of L;
theorem Th28:
x in B implies f.x [= FinJoin(B,f)
by SETWISEO:22;
theorem Th29:
(ex x st x in B & u [= f.x) implies u [= FinJoin(B,f)
proof
given x such that
A1: x in B and
A2: u [= f.x;
f.x [= FinJoin(B,f) by A1,Th28;
then
A3: f.x "\/" FinJoin(B,f) = FinJoin(B,f);
then u "\/" FinJoin(B,f) = u "\/" f.x "\/" FinJoin(B,f) by LATTICES:def 5
.= FinJoin(B,f) by A2,A3;
hence thesis;
end;
theorem
(for x st x in B holds f.x = u) & B <> {} implies FinJoin(B,f) = u by
SETWISEO:24;
theorem
FinJoin(B,f) [= u implies for x st x in B holds f.x [= u
proof
assume
A1: FinJoin(B,f) [= u;
let x;
assume x in B;
then f.x [= FinJoin(B,f) by Th28;
hence thesis by A1,LATTICES:7;
end;
theorem Th32:
B <> {} & (for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u
proof
assume that
A1: B <> {} and
A2: for x st x in B holds f.x [= u;
set J = the L_join of L;
A3: now
let x;
assume x in B;
then
A4: f.x [= u by A2;
thus (J[:](f,u)).x = f.x "\/" u by FUNCOP_1:48
.= u by A4;
end;
FinJoin(B,f) "\/" u = J$$(B,J[:](f,u)) by A1,Th20,SETWISEO:28
.= u by A1,A3,SETWISEO:24;
hence thesis;
end;
theorem
B <> {} & (for x st x in B holds f.x [= g.x) implies FinJoin(B,f) [=
FinJoin(B,g)
proof
assume that
A1: B <> {} and
A2: for x st x in B holds f.x [= g.x;
now
let x;
assume
A3: x in B;
then f.x [= g.x by A2;
hence f.x [= FinJoin(B,g) by A3,Th29;
end;
hence thesis by A1,Th32;
end;
theorem Th34:
B <> {} & f|B = g|B implies FinJoin(B,f) = FinJoin(B,g)
proof
assume that
A1: B <> {} and
A2: f|B = g|B;
f.:B = g.:B by A2,RELAT_1:166;
hence thesis by A1,SETWISEO:26;
end;
theorem
B <> {} implies v "\/" FinJoin(B,f) = FinJoin(B, (the L_join of L)[;](
v, f ) ) by Th20,SETWISEO:27;
registration
let L be Lattice;
cluster L.: -> Lattice-like;
coherence
proof
the L_join of L.: absorbs the L_meet of L.: & the L_meet of L.:
absorbs the L_join of L.: by Th26,Th27;
hence thesis by Th11;
end;
end;
theorem
for L being Lattice, B being Element of Fin A for f being Function
of A, the carrier of L, f9 being Function of A, the carrier of L.: st f = f9
holds FinJoin(B,f) = FinMeet(B,f9) & FinMeet(B,f) = FinJoin(B,f9);
theorem Th37:
for a9,b9 being Element of L.: st a = a9 & b = b9 holds a "/\" b
= a9"\/" b9 & a "\/" b = a9"/\" b9;
theorem Th38:
a [= b implies for a9,b9 being Element of L.: st a = a9 & b = b9
holds b9 [= a9
proof
assume a [= b;
then
A1: a "\/" b = b;
let a9,b9 be Element of L.:;
assume a = a9 & b = b9;
then b9 "/\" a9 = b9 by A1,Th37;
hence thesis by LATTICES:4;
end;
theorem Th39:
for a9,b9 being Element of L.: st a9 [= b9 & a = a9 & b = b9 holds b [= a
proof
let a9,b9 be Element of L.:;
assume that
A1: a9 [= b9 and
A2: a = a9 & b = b9;
a9 "\/" b9 = b9 by A1;
then b "/\" a = b by A2,Th37;
hence thesis by LATTICES:4;
end;
:: Dualizations
theorem Th40:
x in B implies FinMeet(B,f) [= f.x
proof
reconsider f9 = f as Function of A, the carrier of L.:;
assume x in B;
then f9.x [= FinJoin(B,f9) by Th28;
hence thesis by Th39;
end;
theorem Th41:
(ex x st x in B & f.x [= u) implies FinMeet(B,f)[= u
proof
given x such that
A1: x in B and
A2: f.x [= u;
reconsider u9 = u as Element of L.:;
reconsider f9 = f as Function of A, the carrier of L.:;
u9 [= f9.x by A2,Th38;
then u9 [= FinJoin(B,f9) by A1,Th29;
hence thesis by Th39;
end;
theorem
(for x st x in B holds f.x = u) & B <> {} implies FinMeet(B,f) = u
by SETWISEO:24;
theorem
B <> {} implies v "/\" FinMeet(B,f) = FinMeet(B, (the L_meet of L)[;](
v, f ) ) by Th25,SETWISEO:27;
theorem
u [= FinMeet(B,f) implies for x st x in B holds u [= f.x
proof
assume
A1: u [= FinMeet(B,f);
let x;
assume x in B;
then FinMeet(B,f) [= f.x by Th40;
hence thesis by A1,LATTICES:7;
end;
theorem
B <> {} & f|B = g|B implies FinMeet(B,f) = FinMeet(B,g)
proof
reconsider f9 = f, g9 = g as Function of A, the carrier of L.:;
A1: FinMeet(B,f) = FinJoin(B,f9) & FinMeet(B,g) = FinJoin(B,g9);
assume B <> {} & f|B = g|B;
hence thesis by A1,Th34;
end;
theorem Th46:
B <> {} & (for x st x in B holds u [= f.x) implies u [= FinMeet( B,f)
proof
assume that
A1: B <> {} and
A2: for x st x in B holds u [= f.x;
reconsider u9 = u as Element of L.:;
reconsider f9 = f as Function of A, the carrier of L.:;
for x st x in B holds f9.x [= u9 by A2,Th38;
then FinJoin(B,f9) [= u9 by A1,Th32;
hence thesis by Th39;
end;
theorem
B <> {} & (for x st x in B holds f.x [= g.x) implies FinMeet(B,f) [=
FinMeet(B,g)
proof
assume that
A1: B <> {} and
A2: for x st x in B holds f.x [= g.x;
now
let x;
assume
A3: x in B;
then f.x [= g.x by A2;
hence FinMeet(B,f) [= g.x by A3,Th41;
end;
hence thesis by A1,Th46;
end;
theorem
for L being Lattice holds L is lower-bounded iff L.: is upper-bounded
proof
let L be Lattice;
thus L is lower-bounded implies L.: is upper-bounded
proof
given c being Element of L such that
A1: for a being Element of L holds c"/\"a = c & a"/\"c = c;
reconsider c9 = c as Element of L.:;
take c9;
let a9 be Element of L.:;
reconsider a = a9 as Element of L;
thus c9"\/"a9 = c"/\"a .= c9 by A1;
hence a9"\/"c9 = c9;
end;
given c being Element of L.: such that
A2: for a being Element of L.: holds c"\/"a = c & a"\/"c = c;
reconsider c9= c as Element of L;
take c9;
let a9 be Element of L;
reconsider a = a9 as Element of L.:;
thus c9"/\"a9 = c"\/"a .= c9 by A2;
hence a9"/\"c9 = c9;
end;
theorem Th49:
for L being Lattice holds L is upper-bounded iff L.: is lower-bounded
proof
let L be Lattice;
thus L is upper-bounded implies L.: is lower-bounded
proof
given c being Element of L such that
A1: for a being Element of L holds c"\/"a = c & a"\/"c = c;
reconsider c9 = c as Element of L.:;
take c9;
let a9 be Element of L.:;
reconsider a = a9 as Element of L;
thus c9"/\"a9 = c"\/"a .= c9 by A1;
hence a9"/\"c9 = c9;
end;
given c being Element of L.: such that
A2: for a being Element of L.: holds c"/\"a = c & a"/\"c = c;
reconsider c9= c as Element of L;
take c9;
let a9 be Element of L;
reconsider a = a9 as Element of L.:;
thus c9"\/"a9 = c"/\"a .= c9 by A2;
hence a9"\/"c9 = c9;
end;
theorem
L is D_Lattice iff L.: is D_Lattice by Th22,Th23;
::
:: Lower bounded lattices
::
reserve L for 0_Lattice,
f,g for Function of A, the carrier of L,
u for Element of L;
theorem Th51:
Bottom L is_a_unity_wrt the L_join of L
proof
now
let u;
thus (the L_join of L).(Bottom L,u) = Bottom L"\/" u .= u;
end;
hence thesis by BINOP_1:4;
end;
registration
let L;
cluster the L_join of L -> having_a_unity;
coherence
proof
Bottom L is_a_unity_wrt the L_join of L by Th51;
hence thesis;
end;
end;
theorem
Bottom L = the_unity_wrt the L_join of L by Th18;
theorem Th53:
f|B = g|B implies FinJoin(B,f) = FinJoin(B,g)
proof
set J = the L_join of L;
A1: Bottom L = the_unity_wrt J by Th18;
assume
A2: f|B = g|B;
now
per cases;
suppose
A3: B = {};
hence FinJoin(B,f) = J$$({}.A,f) .= Bottom L by A1,SETWISEO:31
.= J$$({}.A,g) by A1,SETWISEO:31
.= FinJoin(B,g) by A3;
end;
suppose
B <> {};
hence thesis by A2,Th34;
end;
end;
hence thesis;
end;
theorem Th54:
(for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u
proof
assume
A1: for x st x in B holds f.x [= u;
set J = the L_join of L;
A2: Bottom L = the_unity_wrt J by Th18;
now
per cases;
suppose
B = {};
then FinJoin(B,f) = J$$({}.A,f) .= Bottom L by A2,SETWISEO:31;
hence thesis;
end;
suppose
B <> {};
hence thesis by A1,Th32;
end;
end;
hence thesis;
end;
theorem
(for x st x in B holds f.x [= g.x) implies FinJoin(B,f) [= FinJoin(B,g )
proof
assume
A1: for x st x in B holds f.x [= g.x;
now
let x;
assume
A2: x in B;
then f.x [= g.x by A1;
hence f.x [= FinJoin(B,g) by A2,Th29;
end;
hence thesis by Th54;
end;
::
:: Upper bounded lattices
::
reserve L for 1_Lattice,
f,g for Function of A, the carrier of L,
u for Element of L;
theorem Th56:
Top L is_a_unity_wrt the L_meet of L
proof
now
let u;
thus (the L_meet of L).(Top L,u) = Top L"/\" u .= u;
end;
hence thesis by BINOP_1:4;
end;
registration
let L;
cluster the L_meet of L -> having_a_unity;
coherence
proof
Top L is_a_unity_wrt the L_meet of L by Th56;
hence thesis;
end;
end;
theorem
Top L = the_unity_wrt the L_meet of L by Th19;
theorem
f|B = g|B implies FinMeet(B,f) = FinMeet(B,g)
proof
assume
A1: f|B = g|B;
reconsider f9 = f, g9 = g as Function of A, the carrier of L.:;
A2: FinMeet(B,g) = FinJoin(B,g9);
L.: is 0_Lattice & FinMeet(B,f) = FinJoin(B,f9) by Th49;
hence thesis by A1,A2,Th53;
end;
theorem Th59:
(for x st x in B holds u [= f.x) implies u [= FinMeet(B,f)
proof
reconsider f9 = f as Function of A, the carrier of L.:;
reconsider u9 = u as Element of L.:;
assume for x st x in B holds u [= f.x;
then
A1: for x st x in B holds f9.x [= u9 by Th38;
L.: is 0_Lattice by Th49;
then FinJoin(B,f9) [= u9 by A1,Th54;
hence thesis by Th39;
end;
theorem
(for x st x in B holds f.x [= g.x) implies FinMeet(B,f) [= FinMeet(B,g )
proof
assume
A1: for x st x in B holds f.x [= g.x;
now
let x;
assume
A2: x in B;
then f.x [= g.x by A1;
hence FinMeet(B,f) [= g.x by A2,Th41;
end;
hence thesis by Th59;
end;
theorem
for L being 0_Lattice holds Bottom L = Top (L.:)
proof
let L be 0_Lattice;
reconsider u = Bottom L as Element of L.:;
now
let v be Element of L.:;
reconsider v9 = v as Element of L;
thus v "\/" u = Bottom L "/\" v9 by Th37
.= u;
end;
hence thesis by RLSUB_2:65;
end;
theorem
for L being 1_Lattice holds Top L = Bottom (L.:)
proof
let L be 1_Lattice;
reconsider u = Top L as Element of L.:;
now
let v be Element of L.:;
reconsider v9 = v as Element of L;
thus v "/\" u = Top L "\/" v9 by Th37
.= u;
end;
hence thesis by RLSUB_2:64;
end;
::
:: Distributive lattices with the minimal element
::
definition
mode D0_Lattice is distributive lower-bounded Lattice;
end;
reserve L for D0_Lattice,
f,g for (Function of A, the carrier of L),
u for Element of L;
theorem
the L_meet of L is_distributive_wrt the L_join of L by Th23;
theorem Th64:
(the L_meet of L).(u, FinJoin(B, f)) = FinJoin(B, (the L_meet of L)[;](u,f))
proof
A1: (the L_meet of L).(u,Bottom L) = u"/\"Bottom L .= Bottom L;
the L_meet of L is_distributive_wrt the L_join of L & Bottom L =
the_unity_wrt the L_join of L by Th18,Th23;
hence thesis by A1,SETWOP_2:12;
end;
theorem
(for x st x in B holds g.x = u "/\" f.x) implies u "/\" FinJoin(B,f) =
FinJoin(B,g)
proof
reconsider G = ((the L_meet of L)[;](u,f)) +* (g|B) as Function of A, the
carrier of L by Th3;
dom (g|B) = B by Th9;
then
A1: G|B = g|B by FUNCT_4:23;
assume
A2: for x st x in B holds g.x = u "/\" f.x;
now
let x;
assume x in B;
hence g.x = u "/\" f.x by A2
.= ((the L_meet of L)[;](u,f)).x by FUNCOP_1:53;
end;
then G = (the L_meet of L)[;](u,f) by Th10;
hence u "/\" FinJoin(B,f) = FinJoin(B,G) by Th64
.= FinJoin(B,g) by A1,Th53;
end;
theorem
u "/\" FinJoin(B,f) = FinJoin(B, (the L_meet of L)[;](u, f)) by Th64;
:: Heyting Lattices
definition
let IT be Lattice;
attr IT is Heyting means
IT is implicative lower-bounded;
end;
registration
cluster Heyting for Lattice;
existence
proof
set L = the B_Lattice;
take L;
thus L is implicative lower-bounded;
end;
end;
registration
cluster Heyting -> implicative lower-bounded for Lattice;
coherence;
cluster implicative lower-bounded -> Heyting for Lattice;
coherence;
end;
definition
mode H_Lattice is Heyting Lattice;
end;
registration
cluster Heyting strict for Lattice;
existence
proof
set L = the strict B_Lattice;
L is I_Lattice;
hence thesis;
end;
end;
theorem
for L being 0_Lattice holds L is H_Lattice iff for x,z being Element
of L ex y being Element of L st x "/\" y [= z & for v being Element of L st x
"/\" v [= z holds v [= y
proof
let L be 0_Lattice;
L is H_Lattice iff L is I_Lattice;
hence thesis by FILTER_0:def 6;
end;
theorem
for L being Lattice holds L is finite iff L.: is finite;
registration
cluster finite -> lower-bounded for Lattice;
coherence
proof
let L be Lattice;
assume L is finite;
then reconsider
B = the carrier of L as Element of Fin the carrier of L by FINSUB_1:def 5;
take c = FinMeet(B,id the carrier of L);
let a be Element of L;
(id the carrier of L).a [= a;
then
A1: c [= a by Th41;
hence c"/\"a = c by LATTICES:4;
thus a"/\"c = c by A1,LATTICES:4;
end;
cluster finite -> upper-bounded for Lattice;
coherence
proof
let L be Lattice;
assume L is finite;
then reconsider
B = the carrier of L as Element of Fin the carrier of L by FINSUB_1:def 5;
take c = FinJoin(B,id the carrier of L);
let a be Element of L;
a [= (id the carrier of L).a;
then
A2: a [= c by Th29;
hence c"\/"a = c;
thus a"\/"c = c by A2;
end;
end;
registration
cluster finite -> bounded for Lattice;
coherence;
end;
registration
cluster distributive finite -> Heyting for Lattice;
coherence
proof
let L be Lattice;
assume
A1: L is distributive finite;
then reconsider L as D0_Lattice;
set C = the carrier of L;
L is implicative
proof
let p,q be Element of C;
defpred X[Element of C] means p "/\" $1 [= q;
set B = {x where x is Element of C: X[x] };
A2: B c= C from FRAENKEL:sch 10;
then B is finite by A1,FINSET_1:1;
then reconsider B as Element of Fin C by A2,FINSUB_1:def 5;
take r = FinJoin(B,id C);
A3: now
let x be Element of C;
assume x in B;
then
A4: ex x9 being Element of C st x9 = x & p "/\" x9 [= q;
((the L_meet of L)[;](p,id C)).x = (the L_meet of L).(p,(id C).x)
by FUNCOP_1:53
.= p "/\" x;
hence ((the L_meet of L)[;](p,id C)).x [= q by A4;
end;
p "/\" r = FinJoin(B,(the L_meet of L)[;](p,id C)) by Th64;
hence p "/\" r [= q by A3,Th54;
let r1 be Element of C;
assume p "/\" r1 [= q;
then
A5: r1 in B;
r1 = (id C).r1;
hence r1 [= r by A5,Th28;
end;
hence thesis;
end;
end;