:: Ideals
:: by Grzegorz Bancerek
::
:: Received October 24, 1994
:: Copyright (c) 1994-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, SUBSET_1, BINOP_1, REALSET1, RELAT_1, ZFMISC_1,
FUNCT_1, LATTICE2, LATTICES, STRUCT_0, EQREL_1, PBOOLE, LATTICE4,
FILTER_0, CARD_FIL, CAT_1, TARSKI, INT_2, YELLOW11, LATTICE5, NAT_LAT,
XBOOLEAN, XXREAL_2, FILTER_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
DOMAIN_1, BINOP_1, REALSET1, LATTICES, NAT_LAT, FILTER_0, LATTICE2,
MCART_1, LATTICE4;
constructors BINOP_1, REALSET1, FILTER_0, LATTICE2, NAT_LAT, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, STRUCT_0, LATTICES,
FILTER_0, LATTICE2, NAT_LAT;
requirements SUBSET, BOOLE;
definitions BINOP_1, LATTICES, LATTICE2, FILTER_0, TARSKI, XBOOLE_0;
equalities BINOP_1, LATTICES, LATTICE2, FILTER_0, REALSET1;
expansions LATTICES, TARSKI, XBOOLE_0;
theorems TARSKI, ZFMISC_1, DOMAIN_1, FUNCT_1, FUNCT_2, BINOP_1, SUBSET_1,
NAT_LAT, LATTICES, FILTER_0, LATTICE2, RELSET_1, RELAT_1;
begin :: Some Properties of the Restriction of Binary Operations
theorem Th1:
for D being non empty set, S being non empty Subset of D, f being
BinOp of D, g being BinOp of S st g = f||S holds (f is commutative implies g is
commutative) & (f is idempotent implies g is idempotent) & (f is associative
implies g is associative)
proof
let D be non empty set, S be non empty Subset of D;
let f be BinOp of D, g be BinOp of S;
A1: dom g = [:S,S:] by FUNCT_2:def 1;
assume
A2: g = f||S;
thus f is commutative implies g is commutative
proof
assume
A3: for a,b being Element of D holds f.(a,b) = f.(b,a);
let a,b be Element of S qua non empty set;
reconsider a9 = a, b9 = b as Element of S;
reconsider a9, b9 as Element of D;
thus g.(a,b) = f.[a,b] by A2,A1,FUNCT_1:47
.= f.(a9,b9)
.= f.(b9,a9) by A3
.= g.[b,a] by A2,A1,FUNCT_1:47
.= g.(b,a);
end;
thus f is idempotent implies g is idempotent
proof
assume
A4: for a being Element of D holds f.(a,a) = a;
let a be Element of S;
thus g.(a,a) = f.[a,a] by A2,A1,FUNCT_1:47
.= f.(a,a)
.= a by A4;
end;
assume
A5: for a,b,c being Element of D holds f.(f.(a,b),c) = f.(a,f.(b,c));
let a,b,c be Element of S qua non empty set;
reconsider a9 = a, b9 = b, c9 = c as Element of S;
reconsider a9, b9, c9 as Element of D;
thus g.(g.(a,b),c) = f.[g.(a,b),c] by A2,A1,FUNCT_1:47
.= f.[f.[a,b],c] by A2,A1,FUNCT_1:47
.= f.(f.(a,b),c)
.= f.(a9,f.(b9,c9)) by A5
.= f.(a,g.[b,c]) by A2,A1,FUNCT_1:47
.= f.[a,g.(b,c)]
.= g.(a,g.(b,c)) by A2,A1,FUNCT_1:47;
end;
theorem
for D being non empty set, S being non empty Subset of D, f being
BinOp of D, g being BinOp of S for d being Element of D, d9 being Element of S
st g = f||S & d9 = d holds (d is_a_left_unity_wrt f implies d9
is_a_left_unity_wrt g) & (d is_a_right_unity_wrt f implies d9
is_a_right_unity_wrt g) & (d is_a_unity_wrt f implies d9 is_a_unity_wrt g)
proof
let D be non empty set, S be non empty Subset of D, f be BinOp of D;
let g be BinOp of S, d be Element of D, d9 be Element of S such that
A1: g = f||S and
A2: d9 = d;
A3: dom g = [:S,S:] by FUNCT_2:def 1;
thus d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g
proof
assume
A4: for a being Element of D holds f.(d,a) = a;
let a be Element of S;
thus g.(d9,a) = f.[d9,a] by A1,A3,FUNCT_1:47
.= f.(d,a) by A2
.= a by A4;
end;
thus d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g
proof
assume
A5: for a being Element of D holds f.(a,d) = a;
let a be Element of S;
thus g.(a,d9) = f.[a,d9] by A1,A3,FUNCT_1:47
.= f.(a,d) by A2
.= a by A5;
end;
assume
A6: d is_a_unity_wrt f;
now
let s be Element of S;
reconsider s9 = s as Element of D;
A7: dom g = [:S,S:] by FUNCT_2:def 1;
[d9,s] in [:S,S:];
hence g.(d9,s) = f.(d,s9) by A1,A2,A7,FUNCT_1:47
.= s by A6,BINOP_1:3;
[s,d9] in [:S,S:];
hence g.(s,d9) = f.(s9,d) by A1,A2,A7,FUNCT_1:47
.= s by A6,BINOP_1:3;
end;
hence thesis by BINOP_1:3;
end;
theorem Th3:
for D being non empty set, S being non empty Subset of D, f1,f2
being BinOp of D, g1,g2 being BinOp of S st g1 = f1||S & g2 = f2||S holds (f1
is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2) & (f1
is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2)
proof
let D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D, g1,
g2 be BinOp of S such that
A1: g1 = f1||S and
A2: g2 = f2||S;
thus f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2
proof
assume
A3: for a,b,c being Element of D holds f1.(a,f2.(b,c)) = f2.(f1.(a,b),
f1.(a,c));
let a,b,c be Element of S;
set ab = g1.(a,b), ac = g1.(a,c), bc = g2.(b,c);
reconsider a9 = a, b9 = b, c9 = c as Element of D;
A4: f2.[b9,c9] = f2.(b9,c9 ) & f1.[a9,b9] = f1.(a9,b9);
A5: f1.[a9,c9] = f1.(a9,c9) & f1.[a,bc] = f1.(a,bc);
dom g2 = [:S,S:] by FUNCT_2:def 1;
then
A6: g2.[b,c] = f2.[b,c] & g2.[ab,ac] = f2.[ab,ac] by A2,FUNCT_1:47;
A7: f2.[ab,ac] = f2.(ab,ac);
A8: dom g1 = [:S,S:] by FUNCT_2:def 1;
then
A9: g1.[a,bc] = f1.[a,bc] by A1,FUNCT_1:47;
g1.[a,b] = f1.[a,b] & g1.[a,c] = f1.[a,c] by A1,A8,FUNCT_1:47;
hence g1.(a,g2.(b,c)) = g2.(g1.(a,b),g1.(a,c)) by A3,A4,A9,A5,A6,A7;
end;
assume
A10: for a,b,c being Element of D holds f1.(f2.(a,b),c) = f2.(f1.(a,c),
f1.(b,c));
let a,b,c be Element of S;
set ab = g2.(a,b), ac = g1.(a,c), bc = g1.(b,c);
A11: f2.[ac,bc] = f2.(ac,bc);
A12: dom g1 = [:S,S:] by FUNCT_2:def 1;
then
A13: g1.[ab,c] = f1.[ab,c] by A1,FUNCT_1:47;
dom g2 = [:S,S:] by FUNCT_2:def 1;
then
A14: g2.[a,b] = f2.[a,b] & g2.[ac,bc] = f2.[ac,bc] by A2,FUNCT_1:47;
reconsider a9 = a, b9 = b, c9 = c as Element of D;
A15: f1.[b9,c9] = f1.(b9,c9) & f2.[a9,b9] = f2.(a9,b9);
A16: f1.[a9,c9] = f1.(a9,c9) & f1.[ab,c] = f1.(ab,c);
g1.[b,c] = f1.[b,c] & g1.[a,c] = f1.[a,c] by A1,A12,FUNCT_1:47;
hence g1.(g2.(a,b),c) = g2.(g1.(a,c),g1.(b,c)) by A10,A15,A13,A16,A14,A11;
end;
theorem
for D being non empty set, S being non empty Subset of D, f1,f2 being
BinOp of D, g1,g2 being BinOp of S st g1 = f1||S & g2 = f2||S holds f1
is_distributive_wrt f2 implies g1 is_distributive_wrt g2
proof
let D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D;
let g1,g2 be BinOp of S;
assume g1 = f1||S & g2 = f2||S & f1 is_left_distributive_wrt f2 & f1
is_right_distributive_wrt f2;
hence g1 is_left_distributive_wrt g2 & g1 is_right_distributive_wrt g2 by Th3
;
end;
theorem Th5:
for D being non empty set, S being non empty Subset of D, f1,f2
being BinOp of D, g1,g2 being BinOp of S st g1 = f1||S & g2 = f2||S holds f1
absorbs f2 implies g1 absorbs g2
proof
let D be non empty set, S be non empty Subset of D, f1,f2 be BinOp of D;
let g1,g2 be BinOp of S;
assume that
A1: g1 = f1||S and
A2: g2 = f2||S;
assume
A3: for a,b being Element of D holds f1.(a,f2.(a,b)) = a;
let a,b be Element of S;
A4: dom g2 = [:S,S:] by FUNCT_2:def 1;
dom g1 = [:S,S:] by FUNCT_2:def 1;
hence g1.(a,g2.(a,b)) = f1.[a,g2.(a,b)] by A1,FUNCT_1:47
.= f1.[a,f2.[a,b]] by A2,A4,FUNCT_1:47
.= f1.(a,f2.(a,b))
.= a by A3;
end;
begin :: Closed Subsets of a Lattice
definition
let D be non empty set, X1,X2 be Subset of D;
redefine pred X1 = X2 means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for x being Element of D holds x in X1 iff x in X2;
compatibility by SUBSET_1:3;
end;
deffunc carr(LattStr) = the carrier of $1;
deffunc join(LattStr) = the L_join of $1;
deffunc met(LattStr) = the L_meet of $1;
reserve L for Lattice,
p,q,r for Element of L,
p9,q9,r9 for Element of L.:,
x, y for set;
theorem
for L1,L2 being LattStr st the LattStr of L1 = the LattStr of L2 holds
L1.: = L2.:;
theorem
L .: .: = the LattStr of L;
theorem
for L1,L2 being non empty LattStr st the LattStr of L1 = the LattStr
of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 = a2 & b1
= b2 holds a1"\/"b1 = a2"\/"b2 & a1"/\"b1 = a2"/\"b2 & (a1 [= b1 iff a2 [= b2);
theorem Th9:
for L1,L2 being 0_Lattice st the LattStr of L1 = the LattStr of
L2 holds Bottom L1 = Bottom L2
proof
let L1,L2 be 0_Lattice;
assume
A1: the LattStr of L1 = the LattStr of L2;
then reconsider c = Bottom L1 as Element of L2;
now
let a be Element of L2;
reconsider b = a as Element of L1 by A1;
Bottom L1"/\"b = Bottom L1;
hence c"/\"a = c by A1;
hence a"/\"c = c;
end;
hence thesis by LATTICES:def 16;
end;
theorem Th10:
for L1,L2 being 1_Lattice st the LattStr of L1 = the LattStr of
L2 holds Top L1 = Top L2
proof
let L1,L2 be 1_Lattice;
assume
A1: the LattStr of L1 = the LattStr of L2;
then reconsider c = Top L1 as Element of L2;
now
let a be Element of L2;
reconsider b = a as Element of L1 by A1;
Top L1"\/"b = Top L1;
hence c"\/"a = c by A1;
hence a"\/"c = c;
end;
hence thesis by LATTICES:def 17;
end;
theorem Th11:
for L1,L2 being C_Lattice st the LattStr of L1 = the LattStr of
L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 = a2 & b1 =
b2 & a1 is_a_complement_of b1 holds a2 is_a_complement_of b2
by Th9,Th10;
theorem
for L1,L2 being B_Lattice st the LattStr of L1 = the LattStr of L2 for
a being Element of L1, b being Element of L2 st a = b holds a` = b`
proof
let L1,L2 be B_Lattice such that
A1: the LattStr of L1 = the LattStr of L2;
let a be Element of L1, b be Element of L2 such that
A2: a = b;
reconsider b9 = a` as Element of L2 by A1;
a` is_a_complement_of a by LATTICES:def 21;
then b9 is_a_complement_of b by A1,A2,Th11;
hence thesis by LATTICES:def 21;
end;
theorem
for X being Subset of L st for p,q holds p in X & q in X iff p"/\"q in
X holds X is ClosedSubset of L
proof
let X be Subset of L such that
A1: for p,q holds p in X & q in X iff p"/\"q in X;
for p,q holds p in X & q in X implies p"\/"q in X
proof
let p,q;
p"/\"(p"\/"q) = p by LATTICES:def 9;
hence thesis by A1;
end;
hence thesis by A1,LATTICES:def 24,def 25;
end;
theorem
for X being Subset of L st for p,q holds p in X & q in X iff p
"\/"q in X holds X is ClosedSubset of L
proof
let X be Subset of L such that
A1: for p,q holds p in X & q in X iff p"\/"q in X;
for p,q holds p in X & q in X implies p"/\"q in X
proof
let p,q;
(p"/\"q)"\/"q = q by LATTICES:def 8;
hence thesis by A1;
end;
hence thesis by A1,LATTICES:def 24,def 25;
end;
definition
let L;
mode Ideal of L is non empty initial join-closed Subset of L;
end;
Lm1: for S being non empty Subset of L holds
S is Ideal of L iff for p,q being Element of L holds
p in S & q in S iff p "\/" q in S
proof let S be non empty Subset of L;
thus S is Ideal of L implies
for p,q being Element of L holds p in S & q in S iff p "\/" q in S
by LATTICES:5,def 22,def 25;
assume
A1: for p,q being Element of L holds p in S & q in S iff p "\/" q in S;
S is initial proof let p,q be Element of L such that
A2: p [= q and
A3: q in S;
p "\/" q = q by A2;
hence p in S by A1,A3;
end;
hence thesis by A1,LATTICES:def 25;
end;
theorem Th15:
for L1,L2 being Lattice st the LattStr of L1 = the LattStr of L2
for x st x is Filter of L1 holds x is Filter of L2
proof
let L1,L2 be Lattice such that
A1: the LattStr of L1 = the LattStr of L2;
let x;
assume x is Filter of L1;
then reconsider F = x as Filter of L1;
now
let a,b be Element of L2;
reconsider a9 = a, b9 = b as Element of L1 by A1;
a"/\"b = a9"/\"b9 by A1;
hence a in F & b in F iff a"/\"b in F by FILTER_0:8;
end;
hence thesis by A1,FILTER_0:8;
end;
theorem Th16:
for L1,L2 being Lattice st the LattStr of L1 = the LattStr of L2
for x st x is Ideal of L1 holds x is Ideal of L2
proof
let L1,L2 be Lattice such that
A1: the LattStr of L1 = the LattStr of L2;
let x;
assume x is Ideal of L1;
then reconsider F = x as Ideal of L1;
now
let a,b be Element of L2;
reconsider a9 = a, b9 = b as Element of L1 by A1;
a"\/"b = a9"\/"b9 by A1;
hence a in F & b in F iff a"\/"b in F by Lm1;
end;
hence thesis by A1,Lm1;
end;
definition
let L,p;
func p.: -> Element of L.: equals
p;
coherence;
end;
definition
let L;
let p be Element of L.:;
func .:p -> Element of L equals
p;
coherence;
end;
theorem
.:(p.:) = p & ( .:p9).: = p9;
theorem
p"/\"q = p.:"\/"q.: & p"\/"q = p.:"/\"q.: & p9"/\"q9 = .:p9"\/".: q9 &
p9"\/"q9 = .:p9 "/\".:q9;
theorem
(p [= q iff q.: [= p.:) & (p9 [= q9 iff .:q9 [= .:p9) by LATTICE2:38,39;
definition
let L;
let X be Subset of L;
func X.: -> Subset of L.: equals
X;
coherence;
end;
definition
let L;
let X be Subset of L.:;
func .:X -> Subset of L equals
X;
coherence;
end;
registration
let L;
let D be non empty Subset of L;
cluster D.: -> non empty;
coherence;
end;
registration
let L;
let D be non empty Subset of L.:;
cluster .:D -> non empty;
coherence;
end;
registration
let L;
let S be meet-closed Subset of L;
cluster S.: -> join-closed for Subset of L.:;
coherence
proof
S.: is join-closed
proof
let p9,q9;
p9"\/"q9 = .: p9"/\" .:q9;
hence thesis by LATTICES:def 24;
end;
hence thesis;
end;
end;
registration
let L;
let S be join-closed Subset of L;
cluster S.: -> meet-closed for Subset of L.:;
coherence
proof
S.: is meet-closed
proof
let p9,q9;
p9"/\"q9 = .: p9"\/" .:q9;
hence thesis by LATTICES:def 25;
end;
hence thesis;
end;
end;
registration
let L;
let S be meet-closed Subset of L.:;
cluster .:S -> join-closed for Subset of L;
coherence
proof
.:S is join-closed
proof
let p,q;
p"\/"q = p.: "/\" q.:;
hence thesis by LATTICES:def 24;
end;
hence thesis;
end;
end;
registration
let L;
let S be join-closed Subset of L.:;
cluster .:S -> meet-closed for Subset of L;
coherence
proof
.:S is meet-closed
proof
let p,q;
p"/\"q = p.: "\/" q.:;
hence thesis by LATTICES:def 25;
end;
hence thesis;
end;
end;
registration
let L;
let F be final Subset of L;
cluster F.: -> initial for Subset of L.:;
coherence
by LATTICE2:39,LATTICES:def 23;
end;
registration
let L;
let F be initial Subset of L;
cluster F.: -> final for Subset of L.:;
coherence
by LATTICE2:39,LATTICES:def 22;
end;
registration
let L;
let F be final Subset of L.:;
cluster .:F -> initial for Subset of L;
coherence
by LATTICE2:38,LATTICES:def 23;
end;
registration
let L;
let F be initial Subset of L.:;
cluster F.: -> final for Subset of L;
coherence
by LATTICE2:38,LATTICES:def 22;
end;
theorem Th20:
x is Ideal of L iff x is Filter of L.:
proof
thus x is Ideal of L implies x is Filter of L.:
proof
assume x is Ideal of L;
then reconsider I = x as Ideal of L;
reconsider I as non empty Subset of L.:;
I is Filter of L.:
proof
now let p9,q9;
p9"/\"q9 = .:p9"\/".:q9;
hence p9 in I & q9 in I iff p9"/\"q9 in I by Lm1;
end;
hence thesis by FILTER_0:8;
end;
hence thesis;
end;
assume x is Filter of L.:;
then reconsider F = x as Filter of L.:;
reconsider F as non empty Subset of L;
now
let p,q;
p.:"/\"q.: = p"\/"q;
hence p in F & q in F iff p"\/"q in F by FILTER_0:8;
end;
hence thesis by Lm1;
end;
theorem Th21:
for D being non empty Subset of L holds D is Ideal of L iff (for
p,q st p in D & q in D holds p "\/" q in D) & for p,q st p in D & q [= p holds
q in D
proof
let D be non empty Subset of L;
thus D is Ideal of L implies (for p,q st p in D & q in D holds p "\/" q in D
) & for p,q st p in D & q [= p holds q in D
by Lm1;
assume
A1: ( for p,q st p in D & q in D holds p"\/"q in D)& for p,q st p in D &
q [= p holds q in D;
for p,q holds p in D & q in D iff p"\/"q in D by A1,LATTICES:5;
hence thesis by Lm1;
end;
reserve I,J for Ideal of L,
F for Filter of L;
theorem Th22:
p in I implies p"/\"q in I & q"/\"p in I
proof
p"/\"q [= p by LATTICES:6;
hence thesis by Th21;
end;
theorem
ex p st p in I
proof
set i = the Element of I qua non empty Subset of L;
i is Element of L;
hence thesis;
end;
theorem
L is lower-bounded implies Bottom L in I
proof
assume L is lower-bounded;
then Top (L.:) = Bottom L & L.: is upper-bounded by LATTICE2:48,61;
then Bottom L in I.: by FILTER_0:11;
hence thesis;
end;
theorem
L is lower-bounded implies {Bottom L} is Ideal of L
proof
assume L is lower-bounded;
then Top (L.:) = Bottom L & L.: is upper-bounded by LATTICE2:48,61;
then {Bottom L} is Filter of L.: by FILTER_0:12;
hence thesis by Th20;
end;
theorem
{p} is Ideal of L implies L is lower-bounded
proof
assume {p} is Ideal of L;
then {p} is Filter of L.: by Th20;
then L.: is upper-bounded by FILTER_0:13;
hence thesis by LATTICE2:48;
end;
begin :: Ideals Generated by Subsets of a Lattice
theorem Th27:
the carrier of L is Ideal of L
proof
carr(L) is Filter of L.: by FILTER_0:14;
hence thesis by Th20;
end;
definition
let L;
func (.L.> -> Ideal of L equals
the carrier of L;
coherence by Th27;
end;
definition
let L,p;
func (.p.> -> Ideal of L equals
{ q : q [= p };
coherence
proof
set X = { q : q [= p };
p in X;
then reconsider X as non empty set;
X c= carr(L)
proof
let x be object;
assume x in X;
then ex q st x = q & q [= p;
hence thesis;
end;
then reconsider X as non empty Subset of L;
now
let q,r;
thus q in X & r in X implies q"\/"r in X
proof
assume q in X & r in X;
then ( ex r st q = r & r [= p)& ex q st r = q & q [= p;
then q"\/"r [= p by FILTER_0:6;
hence thesis;
end;
assume q"\/"r in X;
then
A1: ex s being Element of L st q"\/"r = s & s [= p;
q [= q"\/"r by LATTICES:5;
then
A2: q [= p by A1,LATTICES:7;
r [= r"\/"q by LATTICES:5;
then r [= p by A1,LATTICES:7;
hence q in X & r in X by A2;
end;
hence thesis by Lm1;
end;
end;
theorem Th28:
q in (.p.> iff q [= p
proof
q in (.p.> iff ex r st q = r & r [= p;
hence thesis;
end;
theorem Th29:
(.p.> = <.p.:.) & (.p.:.> = <.p.)
proof
(.p.> = .:<.p.:.)
proof
let q;
A1: q.: in <.p.:.) iff p.: [= q.: by FILTER_0:15;
q in (.p.> iff q [= p by Th28;
hence thesis by A1,LATTICE2:38,39;
end;
hence (.p.> = <.p.:.);
.:(.p.:.> = <.p.)
proof
let q;
A2: q in <.p.) iff p [= q by FILTER_0:15;
q.: in (.p.:.> iff q.: [= p.: by Th28;
hence thesis by A2,LATTICE2:38,39;
end;
hence thesis;
end;
theorem
p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.>
proof
p"/\"q [= p by LATTICES:6;
hence thesis;
end;
theorem
L is upper-bounded implies (.L.> = (.Top L.>
proof
assume
A1: L is upper-bounded;
then L.: is lower-bounded by LATTICE2:49;
then
A2: <.L.:.) = <.Bottom (L.:).) by FILTER_0:17;
Bottom (L.:) = (Top L).: by A1,LATTICE2:62;
hence thesis by A2,Th29;
end;
definition
let L,I;
attr I is max-ideal means
I <> the carrier of L & for J st I c= J & J <> the carrier of L holds I = J;
end;
theorem Th32:
I is max-ideal iff I.: is being_ultrafilter
proof
thus I is max-ideal implies I.: is being_ultrafilter
proof
assume that
A1: I <> carr(L) and
A2: for J st I c= J & J <> carr(L) holds I = J;
thus I.: <> carr(L.:) by A1;
let F be Filter of L.:;
.:F = F;
hence thesis by A2;
end;
assume that
A3: I.: <> carr(L.:) and
A4: for F being Filter of L.: st I.: c= F & F <> carr(L.:) holds I.: = F;
thus I <> carr(L) by A3;
let J be Ideal of L;
J.: = J;
hence thesis by A4;
end;
theorem
L is upper-bounded implies for I st I <> the carrier of L ex J st I c=
J & J is max-ideal
proof
assume L is upper-bounded;
then
A1: L.: is lower-bounded by LATTICE2:49;
let I;
assume I <> carr(L);
then consider F being Filter of L.: such that
A2: I.: c= F & F is being_ultrafilter by A1,FILTER_0:18;
take .:F;
( .:F).: = .:F;
hence thesis by A2,Th32;
end;
theorem
(ex r st p "\/" r <> p) implies (.p.> <> the carrier of L
proof
given r such that
A1: p"\/"r <> p;
p"\/"r = p.:"/\"r.:;
then <.p.:.) <> carr(L.:) by A1,FILTER_0:19;
hence thesis by Th29;
end;
theorem
L is upper-bounded & p <> Top L implies ex I st p in I & I is max-ideal
proof
assume L is upper-bounded;
then
A1: L.: is lower-bounded & Bottom (L.: ) = Top L by LATTICE2:49,62;
assume p <> Top L;
then consider F being Filter of L.: such that
A2: p.: in F & F is being_ultrafilter by A1,FILTER_0:20;
take .:F;
( .:F).: = .:F;
hence thesis by A2,Th32;
end;
reserve D for non empty Subset of L,
D9 for non empty Subset of L.:;
definition
let L,D;
func (.D.> -> Ideal of L means
:Def9:
D c= it & for I st D c= I holds it c= I;
existence
proof
take I = .:<.D.:.);
thus D c= I by FILTER_0:def 4;
let J;
J.: = J;
hence thesis by FILTER_0:def 4;
end;
uniqueness;
end;
Lm2: for L1,L2 being Lattice, D1 being non empty Subset of L1, D2 being non
empty Subset of L2 st the LattStr of L1 = the LattStr of L2 & D1 = D2 holds <.
D1.) = <.D2.) & (.D1.> = (.D2.>
proof
let L1,L2 be Lattice;
let D1 be non empty Subset of L1, D2 be non empty Subset of L2;
assume that
A1: the LattStr of L1 = the LattStr of L2 and
A2: D1 = D2;
A3: D1 c= <.D1.) & D2 c= <.D2.) by FILTER_0:def 4;
<.D1.) is Filter of L2 & <.D2.) is Filter of L1 by A1,Th15;
hence <.D1.) c= <.D2.) & <.D2.) c= <.D1.) by A2,A3,FILTER_0:def 4;
A4: D1 c= (.D1.> & D2 c= (.D2.> by Def9;
(.D1.> is Ideal of L2 & (.D2.> is Ideal of L1 by A1,Th16;
hence (.D1.> c= (.D2.> & (.D2.> c= (.D1.> by A2,A4,Def9;
end;
theorem Th36:
<.D.:.) = (.D.> & <.D.) = (.D.:.> & <..:D9.) = (.D9.> & <.D9.) = (..: D9.>
proof
A1: for L,D holds <.D.:.) = (.D.>
proof
let L,D;
(.D.>.: = (.D.>;
then
A2: D c= (.D.> implies <.D.:.) c= (.D.> by FILTER_0:def 4;
.:<.D.:.) = <.D.:.);
then D c= <.D.:.) implies (.D.> c= <.D.:.) by Def9;
hence thesis by A2,Def9,FILTER_0:def 4;
end;
<.D .: .:.) = <.D.) & <.( .:D9) .: .:.) = <..:D9.) by Lm2;
hence thesis by A1;
end;
theorem Th37:
(.I.> = I
by Def9;
reserve D1,D2 for non empty Subset of L,
D19,D29 for non empty Subset of L.:;
theorem
(D1 c= D2 implies (.D1.> c= (.D2.>) & (.(.D.>.> c= (.D.>
proof
D2 c= (.D2.> by Def9;
then D1 c= D2 implies D1 c= (.D2.>;
hence thesis by Def9;
end;
theorem
p in D implies (.p.> c= (.D.>
proof
<.p.:.) = (.p.> & <.D.:.) = (.D.> by Th29,Th36;
hence thesis by FILTER_0:23;
end;
theorem
D = {p} implies (.D.> = (.p.>
proof
<.p.:.) = (.p.> & <.D.:.) = (.D.> by Th29,Th36;
hence thesis by FILTER_0:24;
end;
theorem Th41:
L is upper-bounded & Top L in D implies (.D.> = (.L.> & (.D.> =
the carrier of L
proof
assume L is upper-bounded;
then
A1: L.: is lower-bounded & Bottom (L.:) = Top L by LATTICE2:49,62;
assume Top L in D;
then <.D.:.) = <.L.:.) by A1,FILTER_0:25;
hence thesis by Th36;
end;
theorem
L is upper-bounded & Top L in I implies I = (.L.> & I = the carrier of L
proof
(.I.> = I by Th37;
hence thesis by Th41;
end;
definition
let L,I;
attr I is prime means
p "/\" q in I iff p in I or q in I;
end;
theorem Th43:
I is prime iff I.: is prime
proof
thus I is prime implies I.: is prime
proof
assume
A1: p "/\" q in I iff p in I or q in I;
let p9,q9;
p9"\/"q9 = ( .:p9)"/\"( .:q9);
hence thesis by A1;
end;
assume
A2: p9"\/"q9 in I.: iff p9 in I.: or q9 in I.:;
let p,q;
(p.:)"\/"(q.:) = p"/\"q;
hence thesis by A2;
end;
definition
let L,D1,D2;
func D1 "\/" D2 -> Subset of L equals
{ p"\/"q : p in D1 & q in D2 };
coherence
proof
set X = { p"\/"q : p in D1 & q in D2 };
X c= carr(L)
proof
let x be object;
assume x in X;
then ex p,q st x = p"\/"q & p in D1 & q in D2;
hence thesis;
end;
hence thesis;
end;
end;
registration
let L,D1,D2;
cluster D1 "\/" D2 -> non empty;
coherence
proof
set X = { p"\/"q : p in D1 & q in D2 };
set p1 = the Element of D1,p2 = the Element of D2;
p1"\/"p2 in X;
then reconsider X as non empty set;
X = D1 "\/" D2;
hence thesis;
end;
end;
Lm3: for L1,L2 being Lattice, D1,E1 being non empty Subset of L1, D2,E2 being
non empty Subset of L2 st the LattStr of L1 = the LattStr of L2 & D1 = D2 & E1
= E2 holds D1"/\"E1 = D2"/\"E2
proof
let L1,L2 be Lattice, D1,E1 be non empty Subset of L1;
let D2,E2 be non empty Subset of L2 such that
A1: the LattStr of L1 = the LattStr of L2 and
A2: D1 = D2 & E1 = E2;
thus D1"/\"E1 c= D2"/\"E2
proof
let x be object;
assume x in D1"/\"E1;
then consider a,b being Element of L1 such that
A3: x = a"/\"b and
A4: a in D1 & b in E1;
reconsider a9 = a, b9 = b as Element of L2 by A1;
x = a9"/\"b9 by A1,A3;
hence thesis by A2,A4;
end;
let x be object;
assume x in D2"/\"E2;
then consider a,b being Element of L2 such that
A5: x = a"/\"b and
A6: a in D2 & b in E2;
reconsider a9 = a, b9 = b as Element of L1 by A1;
x = a9"/\"b9 by A1,A5;
hence thesis by A2,A6;
end;
theorem Th44:
D1 "\/" D2 = D1.: "/\" D2.: & D1.: "\/" D2.: = D1 "/\" D2 & D19
"\/" D29 = .:D19 "/\" .:D29 & .:D19 "\/" .:D29 = D19 "/\" D29
proof
A1: for L,D1,D2 holds D1"\/"D2 = D1.:"/\"D2.:
proof
let L,D1,D2;
thus D1"\/"D2 c= D1.:"/\"D2.:
proof
let x be object;
assume x in D1"\/"D2;
then consider p,q such that
A2: x = p"\/"q & p in D1 & q in D2;
p"\/"q = p.:"/\"q.:;
hence thesis by A2;
end;
thus D1.:"/\"D2.: c= D1"\/"D2
proof
let x be object;
assume x in D1.:"/\"D2.:;
then consider p9,q9 such that
A3: x = p9"/\"q9 & p9 in D1 & q9 in D2;
.:p9"\/".:q9 = p9"/\"q9;
hence thesis by A3;
end;
end;
A4: ( .:D19).: = .:D19 & ( .:D29).: = .:D29;
D1.: .: "/\" D2.: .: = D1 "/\" D2 & D19.: "/\" D29.: = .:D19 "/\" .: D29
by Lm3;
hence thesis by A1,A4;
end;
theorem
p in D1 & q in D2 implies p"\/"q in D1 "\/" D2 & q"\/"p in D1 "\/" D2;
theorem
x in D1 "\/" D2 implies ex p,q st x = p"\/"q & p in D1 & q in D2;
theorem
D1 "\/" D2 = D2 "\/" D1
proof
let r;
thus r in D1"\/"D2 implies r in D2"\/"D1
proof
assume r in D1"\/"D2;
then ex p,q st r = p"\/"q & p in D1 & q in D2;
hence thesis;
end;
assume r in D2"\/"D1;
then ex p,q st r = p"\/"q & p in D2 & q in D1;
hence thesis;
end;
registration
let L be D_Lattice;
let I1,I2 be Ideal of L;
cluster I1 "\/" I2 -> initial join-closed;
coherence
proof
reconsider K = L.: as D_Lattice by LATTICE2:50;
reconsider J1 = I1.:, J2 = I2.: as Filter of K;
I1"\/"I2 = I1.:"/\"I2.: & J1"/\"J2 = (J1"/\"J2).: by Th44;
hence thesis by Th16;
end;
end;
theorem
(.D1 \/ D2.> = (.(.D1.> \/ D2.> & (.D1 \/ D2.> = (.D1 \/ (.D2.>.>
proof
A1: (.D1 \/ (.D2.>.> = <.(D1 \/ (.D2.>).:.) & (.D2.> = <.D2.:.) by Th36;
A2: (.D1 \/ D2.> = <.(D1 \/ D2).:.) by Th36;
(.(.D1.> \/ D2.> = <.((.D1.> \/ D2).:.) & (.D1.> = <.D1.:.) by Th36;
hence thesis by A1,A2,FILTER_0:34;
end;
theorem
(.I \/ J.> = { r : ex p,q st r [= p"\/"q & p in I & q in J }
proof
A1: J.: = J;
(.I \/ J.> = <.(I \/ J).:.) & I.: = I by Th36;
then
A2: (.I \/ J.> = { r9: ex p9,q9 st p9"/\"q9 [= r9 & p9 in I & q9 in J } by A1,
FILTER_0:35;
thus (.I \/ J.> c= { r : ex p,q st r [= p"\/"q & p in I & q in J }
proof
let x be object;
assume x in (.I \/ J.>;
then consider r9 such that
A3: x = r9 and
A4: ex p9,q9 st p9"/\"q9 [= r9 & p9 in I & q9 in J by A2;
consider p9,q9 such that
A5: p9"/\"q9 [= r9 and
A6: p9 in I & q9 in J by A4;
A7: p9"/\"q9 = .:p9 "\/" .: q9;
.:r9 [= .:(p9"/\"q9) by A5,LATTICE2:39;
hence thesis by A3,A6,A7;
end;
let x be object;
assume x in { r : ex p,q st r [= p"\/"q & p in I & q in J };
then consider r such that
A8: x = r and
A9: ex p,q st r [= p"\/"q & p in I & q in J;
consider p,q such that
A10: r [= p"\/"q and
A11: p in I & q in J by A9;
A12: p"\/"q = p.:"/\" q.:;
(p"\/"q).: [= r.: by A10,LATTICE2:38;
hence thesis by A2,A8,A11,A12;
end;
theorem
I c= I "\/" J & J c= I "\/" J
proof
I"\/"J = I.:"/\"J.: by Th44;
hence thesis by FILTER_0:36;
end;
theorem
(.I \/ J.> = (.I "\/" J.>
proof
A1: (.I"\/"J.> = <.(I"\/"J).:.) by Th36;
(.I \/ J.> = <.(I \/ J).:.) & I.:"/\"J.: = I"\/"J by Th36,Th44;
hence thesis by A1,FILTER_0:37;
end;
reserve B for B_Lattice,
IB,JB for Ideal of B,
a,b for Element of B;
theorem Th52:
L is C_Lattice iff L.: is C_Lattice
proof
A1: L is upper-bounded iff L.: is lower-bounded by LATTICE2:49;
A2: L is lower-bounded iff L.: is upper-bounded by LATTICE2:48;
thus L is C_Lattice implies L.: is C_Lattice
proof
assume
A3: L is C_Lattice;
now
let p9;
consider q such that
A4: q is_a_complement_of .:p9 by A3,LATTICES:def 19;
take r = q.:;
q"\/".: p9 = Top L by A4;
then
A5: q.:"/\"p9 = Top L;
q"/\".:p9 = Bottom L by A4;
then
A6: q.:"\/"p9 = Bottom L;
Top (L.: ) = Bottom L & Bottom (L.:) = Top L by A3,LATTICE2:61,62;
hence r is_a_complement_of p9 by A5,A6;
end;
hence thesis by A2,A1,A3,LATTICES:def 19;
end;
assume
A7: L.: is C_Lattice;
now
let p;
consider q9 such that
A8: q9 is_a_complement_of p.: by A7,LATTICES:def 19;
q9"\/"p.: = Top (L.:) by A8;
then
A9: .:q9"/\"p = Top (L.:);
take r = .:q9;
L is upper-bounded by A7,LATTICE2:49;
then
A10: Bottom (L.:) = Top L by LATTICE2:62;
q9"/\"p.: = Bottom (L.:) by A8;
then
A11: .:q9"\/"p = Bottom (L.:);
L is lower-bounded by A7,LATTICE2:48;
then Top (L.: ) = Bottom L by LATTICE2:61;
hence r is_a_complement_of p by A9,A11,A10;
end;
hence thesis by A2,A1,A7,LATTICES:def 19;
end;
theorem Th53:
L is B_Lattice iff L.: is B_Lattice
proof
A1: L is distributive iff L.: is distributive by LATTICE2:50;
L is C_Lattice iff L.: is C_Lattice by Th52;
hence thesis by A1;
end;
registration
let B be B_Lattice;
cluster B.: -> Boolean Lattice-like;
coherence by Th53;
end;
reserve a9 for Element of (B qua Lattice).:;
Lm4: a.:` = a`
proof
a.:`"/\"a.: = Bottom (B.:) by LATTICES:20;
then
A1: .:(a.:`)"\/".:(a.:) = Top B by LATTICE2:62;
a.:`"\/"a.: = Top (B.:) by LATTICES:21;
then .:(a.:`)"/\".:(a.:) = Bottom B by LATTICE2:61;
then .:(a.:`) is_a_complement_of a by A1;
hence thesis by LATTICES:def 21;
end;
theorem Th54:
a.:` = a` & ( .:a9)` = a9`
proof
( .:a9).: = .:a9;
hence thesis by Lm4;
end;
theorem
(.IB \/ JB.> = IB "\/" JB
proof
reconsider FB = IB.:, GB = JB.: as Filter of B.:;
thus (.IB \/ JB.> = <.(IB \/ JB).:.) by Th36
.= FB"/\"GB by FILTER_0:39
.= IB "\/" JB by Th44;
end;
theorem
IB is max-ideal iff IB <> the carrier of B & for a holds a in IB or a` in
IB
proof
reconsider FB = IB.: as Filter of B.:;
A1: FB is being_ultrafilter iff FB <> carr(B.:) & for a being Element of B.:
holds a in FB or a` in FB by FILTER_0:44;
thus IB is max-ideal implies IB <> carr(B) & for a holds a in IB or a` in
IB
proof
assume
A2: IB is max-ideal;
hence IB <> carr(B);
let a;
reconsider b = a as Element of B.:;
b in FB or b` in FB & a.:` = a` by A1,A2,Th32,Th54;
hence thesis;
end;
assume that
A3: IB <> carr(B) and
A4: for a holds a in IB or a` in IB;
now
let a be Element of B.:;
reconsider b = a as Element of B;
b in FB or b` in FB & ( .:(a qua Element of (B qua Lattice).:))` = a`
by A4,Th54;
hence a in FB or a` in FB;
end;
hence thesis by A1,A3,Th32;
end;
theorem
IB <> (.B.> & IB is prime iff IB is max-ideal
proof
reconsider F = IB.: as Filter of B.:;
<.B.:.) = (.B.>;
then F <> (.B.> & F is prime iff F is being_ultrafilter by FILTER_0:45;
hence thesis by Th32,Th43;
end;
theorem
IB is max-ideal implies for a holds a in IB iff not a` in IB
proof
reconsider FB = IB.: as Filter of B.:;
assume IB is max-ideal;
then
A1: FB is being_ultrafilter by Th32;
let a;
a.:` = a` by Lm4;
hence thesis by A1,FILTER_0:46;
end;
theorem
a <> b implies ex IB st IB is max-ideal & (a in IB & not b in IB or
not a in IB & b in IB)
proof
assume a <> b;
then consider FB being Filter of B.: such that
A1: FB is being_ultrafilter and
A2: a.: in FB & not b.: in FB or not a.: in FB & b.: in FB by FILTER_0:47;
take IB = .:(FB qua Filter of (B qua Lattice).:);
IB.: = FB;
hence IB is max-ideal by A1,Th32;
thus thesis by A2;
end;
reserve P for non empty ClosedSubset of L,
o1,o2 for BinOp of P;
theorem Th60:
(the L_join of L)||P is BinOp of P & (the L_meet of L)||P is BinOp of P
proof
dom join(L) = [:carr(L),carr(L):] by FUNCT_2:def 1;
then
A1: dom(join(L)||P) = [:P,P:] by RELAT_1:62;
rng (join(L)||P) c= P
proof
let x be object;
assume x in rng (join(L)||P);
then consider y being object such that
A2: y in [:P,P:] and
A3: x = (join(L)||P).y by A1,FUNCT_1:def 3;
consider p1,p2 being Element of P such that
A4: y = [p1,p2] by A2,DOMAIN_1:1;
x = p1"\/"p2 by A1,A3,A4,FUNCT_1:47;
hence thesis by LATTICES:def 25;
end;
hence join(L)||P is BinOp of P by A1,FUNCT_2:def 1,RELSET_1:4;
dom met(L) = [:carr(L),carr(L):] by FUNCT_2:def 1;
then
A5: dom (met(L)||P) = [:P,P:] by RELAT_1:62;
rng (met(L)||P) c= P
proof
let x be object;
assume x in rng (met(L)||P);
then consider y being object such that
A6: y in [:P,P:] and
A7: x = (met(L)||P).y by A5,FUNCT_1:def 3;
consider p1,p2 being Element of P such that
A8: y = [p1,p2] by A6,DOMAIN_1:1;
x = p1"/\"p2 by A5,A7,A8,FUNCT_1:47;
hence thesis by LATTICES:def 24;
end;
hence thesis by A5,FUNCT_2:def 1,RELSET_1:4;
end;
theorem Th61:
o1 = (the L_join of L)||P & o2 = (the L_meet of L)||P implies o1
is commutative & o1 is associative & o2 is commutative & o2 is associative & o1
absorbs o2 & o2 absorbs o1 by Th1,Th5,LATTICE2:26,27;
definition
let L,p,q;
assume
A1: p [= q;
func [#p,q#] -> non empty ClosedSubset of L equals
:Def12:
{r: p [= r & r [=
q};
coherence
proof
set P = {r: p [= r & r [= q};
p in P by A1;
then reconsider P as non empty set;
P c= carr(L)
proof
let x be object;
assume x in P;
then ex r st x = r & p [= r & r [= q;
hence thesis;
end;
then reconsider P as non empty Subset of L;
now
let p1,p2 be Element of L;
assume that
A2: p1 in P and
A3: p2 in P;
A4: ex r st p1 = r & p [= r & r [= q by A2;
then
A5: p [= p1"\/"p2 & p1"/\"p2 [= q by FILTER_0:2,3;
ex r st p2 = r & p [= r & r [= q by A3;
then p [= p1"/\"p2 & p1"\/"p2 [= q by A4,FILTER_0:6,7;
hence p1"/\"p2 in P & p1"\/"p2 in P by A5;
end;
then (for p1,p2 being Element of L st p1 in P & p2 in P
holds p1"/\"p2 in P) & for p1,p2 being Element of L st p1 in P & p2 in P
holds p1"\/"p2 in P;
hence thesis by LATTICES:def 24,def 25;
end;
end;
theorem Th62:
p [= q implies (r in [#p,q#] iff p [= r & r [= q)
proof
assume p [= q;
then [#p,q#] = {s where s is Element of L: p [= s & s [= q} by Def12;
then r in [#p,q#] iff ex s being Element of L st r = s & p [= s & s [= q;
hence thesis;
end;
theorem
p [= q implies p in [#p,q#] & q in [#p,q#] by Th62;
theorem
[#p,p#] = {p}
proof
let q;
hereby
assume q in [#p,p#];
then p [= q & q [= p by Th62;
then q = p by LATTICES:8;
hence q in {p} by TARSKI:def 1;
end;
p in [#p,p#] by Th62;
hence thesis by TARSKI:def 1;
end;
theorem
L is upper-bounded implies <.p.) = [#p,Top L#]
proof
assume
A1: L is upper-bounded;
let q;
A2: q in <.p.) iff p [= q by FILTER_0:15;
p [= Top L & q [= Top L by A1,LATTICES:19;
hence thesis by A2,Th62;
end;
theorem
L is lower-bounded implies (.p.> = [#Bottom L,p#]
proof
assume
A1: L is lower-bounded;
let q;
A2: q in (.p.> iff q [= p by Th28;
Bottom L [= p & Bottom L [= q by A1;
hence thesis by A2,Th62;
end;
theorem
for L1,L2 being Lattice for F1 being Filter of L1, F2 being Filter of
L2 st the LattStr of L1 = the LattStr of L2 & F1 = F2 holds latt F1 = latt F2
proof
let L1,L2 be Lattice, F1 be Filter of L1, F2 be Filter of L2;
ex o1,o2 being BinOp of F1 st o1 = (the L_join of L1)||F1 & o2 = (the
L_meet of L1)||F1 & latt F1 = LattStr (#F1, o1, o2#) by FILTER_0:def 9;
hence thesis by FILTER_0:def 9;
end;
begin :: Sublattices
notation
let L;
synonym Sublattice of L for SubLattice of L;
end;
definition
let L;
redefine mode Sublattice of L means :: redefines Sublattice (FILTER_2, synonym) → SubLattice (NAT_LAT, definition)
:Def13:
ex P,o1,o2 st o1 = (the L_join
of L)||P & o2 = (the L_meet of L)||P & the LattStr of it = LattStr (#P, o1, o2
#);
compatibility
proof
let K be Lattice;
thus K is SubLattice of L implies ex P,o1,o2 st o1 = (the L_join of L)||P
& o2 = (the L_meet of L)||P & the LattStr of K = LattStr(#P,o1,o2#)
proof
assume
A1: K is SubLattice of L;
then
A2: met(K) = met(L)||carr(K) by NAT_LAT:def 12;
reconsider P = carr(K) as non empty Subset of L by A1,NAT_LAT:def 12;
A3: join(K) = join(L)||carr(K) by A1,NAT_LAT:def 12;
now
let p,q be Element of L;
assume p in P & q in P;
then
A4: [p,q] in [:P,P:] by ZFMISC_1:87;
dom met(K) = [:P,P:] by FUNCT_2:def 1;
then
A5: met(L).[p,q] = met(K).[p,q] by A2,A4,FUNCT_1:47;
dom join(K) = [:P,P:] by FUNCT_2:def 1;
then join(L).[p,q] = join(K).[p,q] by A3,A4,FUNCT_1:47;
hence p"/\"q in P & p"\/"q in P by A4,A5,FUNCT_2:5;
end;
then (for p1,p2 being Element of L st p1 in P & p2 in P
holds p1"/\"p2 in P) & for p1,p2 being Element of L st p1 in P & p2 in P
holds p1"\/"p2 in P;
then reconsider P as non empty ClosedSubset of L
by LATTICES:def 24,def 25;
take P;
reconsider o1 = join(K), o2 = met(K) as BinOp of P;
take o1, o2;
thus thesis by A1,NAT_LAT:def 12;
end;
given P,o1,o2 such that
A6: o1 = (the L_join of L)||P & o2 = (the L_meet of L)||P & the
LattStr of K = LattStr (#P, o1, o2#);
thus thesis by A6,NAT_LAT:def 12;
end;
end;
theorem Th68:
for K being Sublattice of L, a being Element of K holds a is Element of L
by NAT_LAT:def 12,TARSKI:def 3;
definition
let L,P;
func latt (L,P) -> Sublattice of L means
:Def14:
ex o1,o2 st o1 = (the
L_join of L)||P & o2 = (the L_meet of L)||P & it = LattStr (#P, o1, o2#);
existence
proof
reconsider o1 = join(L)||P, o2 = met(L)||P as BinOp of P by Th60;
o1 = join(L)||P;
then
A1: o2 is commutative associative by Th61;
o2 = met(L)||P;
then
A2: o1 is commutative associative by Th61;
o1 absorbs o2 & o2 absorbs o1 by Th61;
then reconsider K = LattStr (#P, o1, o2#) as strict Lattice by A2,A1,
LATTICE2:11;
reconsider K as strict Sublattice of L by NAT_LAT:def 12;
take K,o1,o2;
thus thesis;
end;
uniqueness;
end;
registration
let L,P;
cluster latt (L,P) -> strict;
coherence
proof
ex o1,o2 st o1 = (the L_join of L)||P & o2 = (the L_meet of L)||P &
latt(L,P) = LattStr (#P, o1, o2#) by Def14;
hence thesis;
end;
end;
definition
let L;
let l be Sublattice of L;
redefine func l.: -> strict Sublattice of L.:; :: redefines .: (LATTICE2, definition)
coherence
proof
consider P, o1, o2 such that
A1: o1 = join(L)||P & o2 = met(L)||P & the LattStr of l = LattStr (#P,
o1, o2#) by Def13;
l.: is Sublattice of L.:
proof
take P.:;
thus thesis by A1;
end;
hence thesis;
end;
end;
theorem Th69:
latt F = latt (L,F)
proof
ex o1, o2 being BinOp of F st o1 = join(L)||F & o2 = met(L)||F & latt (L
,F) = LattStr (#F, o1, o2#) by Def14;
hence thesis by FILTER_0:def 9;
end;
theorem Th70:
latt (L,P) = (latt (L.:,P.:)).:
proof
(ex o1, o2 st o1 = join(L)||P & o2 = met(L)||P & latt (L,P) = LattStr
(#P, o1, o2#) )& ex o3, o4 being BinOp of P.: st o3 = join(L.:)||(P.:) & o4 =
met (L.:)||(P.:) & latt (L.:,P.:) = LattStr (#P.:, o3, o4#) by Def14;
hence thesis;
end;
theorem
latt (L,(.L.>) = the LattStr of L & latt (L,<.L.)) = the LattStr of L
proof
A1: dom met(L) = [:carr(L), carr(L):] & join(L)|(dom join(L) qua set) = join
(L) by FUNCT_2:def 1,RELAT_1:68;
(ex o1,o2 being BinOp of (.L.> st o1 = (the L_join of L)|| (.L.> & o2 =
(the L_meet of L)||(.L.> & latt (L,(.L.>) = LattStr (#(.L.>, o1, o2#) )& dom
join( L) = [:carr(L), carr(L):] by Def14,FUNCT_2:def 1;
hence thesis by A1,RELAT_1:68;
end;
theorem Th72:
the carrier of latt (L,P) = P & the L_join of latt (L,P) = (the
L_join of L)||P & the L_meet of latt (L,P) = (the L_meet of L)||P
proof
ex o1, o2 st o1 = join(L)||P & o2 = met(L)||P & latt (L,P) = LattStr (#P
, o1, o2#) by Def14;
hence thesis;
end;
theorem Th73:
for p,q for p9,q9 being Element of latt (L,P) st p = p9 & q = q9
holds p"\/"q = p9"\/"q9 & p"/\"q = p9"/\"q9
proof
let p,q;
let p9,q9 be Element of latt (L,P);
assume
A1: p = p9 & q = q9;
consider o1, o2 such that
A2: o1 = join(L)||P and
A3: o2 = met(L)||P and
A4: latt (L,P) = LattStr (#P, o1, o2#) by Def14;
A5: [p9,q9] in [:P,P:] by A4;
dom o1 = [:P,P:] by FUNCT_2:def 1;
hence p"\/"q = p9"\/"q9 by A1,A2,A4,A5,FUNCT_1:47;
dom o2 = [:P,P:] by FUNCT_2:def 1;
hence thesis by A1,A3,A4,A5,FUNCT_1:47;
end;
theorem Th74:
for p,q for p9,q9 being Element of latt (L,P) st p = p9 & q = q9
holds p [= q iff p9 [= q9
by Th73;
theorem
L is lower-bounded implies latt (L,I) is lower-bounded
proof
set b9 = the Element of latt (L,I);
reconsider b = b9 as Element of L by Th68;
given c being Element of L such that
A1: for a being Element of L holds c"/\"a = c & a"/\"c = c;
A2: carr(latt (L,I)) = I by Th72;
c"/\"b = c by A1;
then reconsider c9 = c as Element of latt (L,I) by A2,Th22;
take c9;
let a9 be Element of latt (L,I);
reconsider a = a9 as Element of L by Th68;
thus c9"/\"a9 = c"/\"a by Th73
.= c9 by A1;
hence a9"/\"c9 = c9;
end;
theorem
L is modular implies latt (L,P) is modular
proof
assume
A1: for a,b,c being Element of L st a [= c holds a"\/"(b"/\"c) = (a"\/"b
)"/\"c;
let a9,b9,c9 be Element of latt (L,P);
reconsider a = a9, b = b9, c = c9, bc = b9"/\"c9, ab = a9"\/"b9 as Element
of L by Th68;
assume a9 [= c9;
then
A2: a [= c by Th74;
thus a9"\/"(b9"/\"c9) = a"\/"bc by Th73
.= a"\/"(b"/\"c) by Th73
.= (a"\/"b)"/\"c by A1,A2
.= ab"/\"c by Th73
.= (a9"\/"b9)"/\"c9 by Th73;
end;
theorem Th77:
L is distributive implies latt (L,P) is distributive
proof
assume
A1: for a,b,c being Element of L holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a "/\"c);
let a9,b9,c9 be Element of latt (L,P);
reconsider a = a9, b = b9, c = c9, bc = b9"\/"c9, ab = a9"/\"b9, ac = a9"/\"
c9 as Element of L by Th68;
thus a9"/\"(b9"\/"c9) = a"/\"bc by Th73
.= a"/\"(b"\/"c) by Th73
.= (a"/\"b)"\/"(a"/\"c) by A1
.= ab"\/"(a"/\"c) by Th73
.= ab"\/" ac by Th73
.= (a9"/\"b9)"\/"(a9"/\"c9) by Th73;
end;
theorem
L is implicative & p [= q implies latt (L,[#p,q#]) is implicative
proof
assume
A1: L is implicative;
set P = [#p,q#], K = latt (L,P);
assume
A2: p [= q;
let a9,b9 be Element of latt (L,P);
reconsider a = a9, b = b9 as Element of L by Th68;
set c = a => b;
A3: carr(K) = P by Th72;
then p [= a by A2,Th62;
then
A4: p"\/"(c"/\"a) = (p"\/"c)"/\"a by A1,LATTICES:def 12;
A5: a"/\"c [= b by A1,FILTER_0:def 7;
p [= b by A2,A3,Th62;
then p"\/"(a"/\"c) [= b by A5,FILTER_0:6;
then
A6: (p"\/"(a"/\"c))"/\"q [= b by FILTER_0:2;
set d = (c"\/"p)"/\"q;
p [= c"\/"p by LATTICES:5;
then d [= q & p [= d by A2,FILTER_0:7,LATTICES:6;
then reconsider d9 = d as Element of K by A2,A3,Th62;
take d9;
(p"\/"c)"/\"a"/\"q = a"/\"d & a"/\"d = a9 "/\"d9 by Th73,LATTICES:def 7;
hence a9"/\"d9 [= b9 by A4,A6,Th74;
let e9 be Element of K;
reconsider e = e9, ae = a9"/\"e9 as Element of L by Th68;
e [= q by A2,A3,Th62;
then
A7: e = e"/\"q by LATTICES:4;
assume a9"/\"e9 [= b9;
then ae [= b by Th74;
then a"/\"e [= b by Th73;
then
A8: e [= c by A1,FILTER_0:def 7;
p [= e by A2,A3,Th62;
then e = e"\/"p;
then e [= c"\/"p by A8,FILTER_0:1;
then e [= d by A7,LATTICES:9;
hence e9 [= d9 by Th74;
end;
registration
let L,p;
cluster latt (L,(.p.>) -> upper-bounded;
coherence
proof
latt (L,(.p.>) = (latt (L.:,(.p.>.:)).: by Th70
.= (latt (L.:,<.p.:.))).: by Th29
.= (latt <.p.:.)).: by Th69;
hence thesis by LATTICE2:48;
end;
end;
theorem Th79:
Top latt (L,(.p.>) = p
proof
latt (L,(.p.>) = (latt (L.:,(.p.>.:)).: by Th70
.= (latt (L.:,<.p.:.))).: by Th29
.= (latt <.p.:.)).: by Th69;
hence Top latt (L,(.p.>) = Bottom latt <.p.:.) by LATTICE2:61
.= p by FILTER_0:56;
end;
theorem Th80:
L is lower-bounded implies latt (L,(.p.>) is lower-bounded &
Bottom latt (L,(.p.>) = Bottom L
proof
assume
A1: L is lower-bounded;
then
A2: L.: is upper-bounded by LATTICE2:48;
then
A3: latt <.p.:.) is upper-bounded by FILTER_0:52;
A4: latt (L,(.p.>) = (latt (L.:,(.p.>.:)).: by Th70
.= (latt (L.:,<.p.:.))).: by Th29
.= (latt <.p.:.)).: by Th69;
hence latt (L,(.p.>) is lower-bounded by A3,LATTICE2:49;
Top latt <.p.:.) = Top (L.:) by A2,FILTER_0:57;
hence Bottom latt (L,(.p.>) = Top (L.:) by A4,A3,LATTICE2:62
.= Bottom L by A1,LATTICE2:61;
end;
theorem Th81:
L is lower-bounded implies latt (L,(.p.>) is bounded
by Th80;
theorem Th82:
p [= q implies latt (L,[#p,q#]) is bounded & Top latt (L,[#p,q#]
) = q & Bottom latt (L,[#p,q#]) = p
proof
assume
A1: p [= q;
A2: carr(latt (L,[#p,q#])) = [#p,q#] by Th72;
then reconsider p9 = p, q9 = q as Element of latt (L,[#p,q#]) by A1,Th62;
A3: now
let a9 be Element of latt (L,[#p,q#]);
reconsider a = a9 as Element of L by Th68;
A4: a [= q by A1,A2,Th62;
thus q9"\/"a9 = q"\/"a by Th73
.= q9 by A4;
hence a9"\/"q9 = q9;
end;
A5: now
let a9 be Element of latt (L,[#p,q#]);
reconsider a = a9 as Element of L by Th68;
A6: p [= a by A1,A2,Th62;
thus p9"/\"a9 = p"/\"a by Th73
.= p9 by A6,LATTICES:4;
hence a9"/\"p9 = p9;
end;
then
A7: latt (L,[#p,q#]) is lower-bounded upper-bounded Lattice by A3,
LATTICES:def 13,def 14;
hence latt (L,[#p,q#]) is bounded;
thus thesis by A5,A3,A7,LATTICES:def 16,def 17;
end;
theorem
L is C_Lattice & L is modular implies latt (L,(.p.>) is C_Lattice
proof
assume that
A1: L is C_Lattice and
A2: L is modular;
reconsider K = latt (L,(.p.>) as bounded Lattice by A1,Th81;
K is complemented
proof
let b9 be Element of K;
reconsider b = b9 as Element of L by Th68;
consider a being Element of L such that
A3: a is_a_complement_of b by A1,LATTICES:def 19;
A4: a"\/"b = Top L by A3;
A5: carr(K) = (.p.> by Th72;
then
A6: b [= p by Th28;
p"/\"a [= p by LATTICES:6;
then reconsider a9 = p"/\"a as Element of K by A5,Th28;
take a9;
thus a9"\/"b9 = (p"/\"a)"\/"b by Th73
.= (b"\/"a)"/\" p by A2,A6
.= p by A1,A4
.= Top K by Th79;
hence b9"\/"a9 = Top K;
A7: a"/\"b = Bottom L by A3;
thus a9"/\"b9 = (p"/\"a)"/\"b by Th73
.= p"/\"Bottom L by A7,LATTICES:def 7
.= Bottom L by A1
.= Bottom K by A1,Th80;
hence thesis;
end;
hence thesis;
end;
theorem Th84:
L is C_Lattice & L is modular & p [= q implies latt (L,[#p,q#]) is C_Lattice
proof
assume that
A1: L is C_Lattice and
A2: L is modular and
A3: p [= q;
reconsider K = latt (L,[#p,q#]) as bounded Lattice by A3,Th82;
K is complemented
proof
let b9 be Element of K;
reconsider b = b9 as Element of L by Th68;
consider a being Element of L such that
A4: a is_a_complement_of b by A1,LATTICES:def 19;
A5: a"/\"b = Bottom L by A4;
A6: a"\/"b = Top L by A4;
A7: carr(K) = [#p,q#] by Th72;
then
A8: b [= q by A3,Th62;
a"/\"q [= q by LATTICES:6;
then p [= p"\/"(a"/\"q) & p"\/"(a"/\"q) [= q by A3,FILTER_0:6,LATTICES:5;
then reconsider a9 = p"\/"(a"/\"q) as Element of K by A3,A7,Th62;
take a9;
A9: p [= b by A3,A7,Th62;
thus a9"\/"b9 = (p"\/"(a"/\"q))"\/"b by Th73
.= b"\/"p"\/"(a"/\" q) by LATTICES:def 5
.= b"\/"(a"/\"q) by A9
.= (Top L)"/\"q by A2,A6,A8
.= q by A1
.= Top K by A3,Th82;
hence b9"\/"a9 = Top K;
thus a9"/\"b9 = (p"\/"(a"/\"q))"/\"b by Th73
.= p"\/"((a"/\"q)"/\"b) by A2,A9
.= p"\/"(q"/\"Bottom L) by A5,LATTICES:def 7
.= p"\/"Bottom L by A1
.= p by A1
.= Bottom K by A3,Th82;
hence thesis;
end;
hence thesis;
end;
theorem
L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice
proof
assume L is B_Lattice & p [= q;
then latt (L,[#p,q#]) is bounded complemented distributive Lattice by Th77
,Th84;
hence thesis;
end;
theorem for S being non empty Subset of L holds
S is Ideal of L iff for p,q being Element of L holds
p in S & q in S iff p "\/" q in S by Lm1;