:: More on the Lattice of Many Sorted Equivalence Relations
:: by Robert Milewski
::
:: Received February 9, 1996
:: Copyright (c) 1996-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 NUMBERS, XBOOLE_0, PBOOLE, REAL_1, STRUCT_0, MSUALG_5, EQREL_1,
RELAT_1, FUNCT_1, MSUALG_4, TARSKI, ZFMISC_1, XXREAL_2, SUBSET_1,
LATTICES, CLOSURE2, SETFAM_1, FUNCT_4, REWRITE1, LATTICE3, MSSUBFAM,
NAT_LAT, REALSET1, XXREAL_0, XXREAL_1, REAL_LAT, BINOP_1, SUPINF_1,
ORDINAL2, ARYTM_1, CARD_1, ARYTM_3, MSUALG_7, SETLIM_2, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SUPINF_1, ORDINAL1, FUNCT_7,
XXREAL_0, REAL_1, XXREAL_2, XCMPLX_0, XREAL_0, STRUCT_0, RELSET_1,
DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, NUMBERS, RCOMP_1, EQREL_1, BINOP_1,
REALSET1, PBOOLE, LATTICES, LATTICE3, NAT_LAT, REAL_LAT, MSUALG_3,
MSUALG_4, MSUALG_5, SETFAM_1, MSSUBFAM, CLOSURE2;
constructors BINOP_1, REAL_1, SQUARE_1, SUPINF_1, RCOMP_1, REALSET1, MSSUBFAM,
REAL_LAT, LATTICE3, MSUALG_3, MSUALG_5, CLOSURE2, XXREAL_2, RELSET_1,
FUNCT_7;
registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, REALSET1, MSSUBFAM, STRUCT_0, LATTICES, LATTICE3, CLOSURE2,
ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, LATTICE3, XXREAL_2;
equalities BINOP_1, REALSET1;
expansions TARSKI, LATTICE3, XXREAL_2;
theorems TARSKI, PBOOLE, MSSUBFAM, LATTICE3, VECTSP_8, MSUALG_4, MSUALG_5,
ZFMISC_1, SETFAM_1, EQREL_1, LATTICES, NAT_LAT, FUNCT_1, REAL_LAT,
FUNCT_2, RCOMP_1, MSUALG_3, CLOSURE2, XBOOLE_0, XBOOLE_1, XREAL_1,
XXREAL_0, NUMBERS, RELAT_1, XXREAL_2, XREAL_0;
schemes DOMAIN_1;
begin :: LATTICE OF MANY SORTED EQUIVALENCE RELATIONS IS COMPLETE
reserve I for non empty set;
reserve M for ManySortedSet of I;
reserve Y,x,y,i for set;
reserve r,r1,r2 for Real;
theorem Th1:
id M is Equivalence_Relation of M
proof
set J = id M;
for i be set st i in I holds J.i is Relation of M.i
proof
let i be set;
assume i in I;
then J.i = id (M.i) by MSUALG_3:def 1;
hence thesis;
end;
then reconsider J as ManySortedRelation of M by MSUALG_4:def 1;
for i be object, R be Relation of M.i st i in I & J.i = R holds R is
Equivalence_Relation of M.i
proof
let i be object;
let R be Relation of M.i;
assume that
A1: i in I and
A2: J.i = R;
J.i = id (M.i) by A1,MSUALG_3:def 1;
hence thesis by A2,EQREL_1:3;
end;
hence thesis by MSUALG_4:def 2;
end;
theorem Th2:
[|M,M|] is Equivalence_Relation of M
proof
set J = [|M,M|];
for i be set st i in I holds J.i is Relation of M.i
proof
let i be set;
assume i in I;
then J.i c= [:M.i,M.i:] by PBOOLE:def 16;
hence thesis;
end;
then reconsider J as ManySortedRelation of M by MSUALG_4:def 1;
for i be object, R be Relation of M.i st i in I & J.i = R holds R is
Equivalence_Relation of M.i
proof
let i be object;
let R be Relation of M.i;
assume that
A1: i in I and
A2: J.i = R;
J.i = [:M.i,M.i:] by A1,PBOOLE:def 16
.= nabla M.i by EQREL_1:def 1;
hence thesis by A2,EQREL_1:4;
end;
hence thesis by MSUALG_4:def 2;
end;
registration
let I,M;
cluster EqRelLatt M -> bounded;
coherence
proof
ex c being Element of EqRelLatt M st for a being Element of EqRelLatt
M holds c"\/"a = c & a"\/"c = c
proof
reconsider c9 = [|M,M|] as Equivalence_Relation of M by Th2;
reconsider c = c9 as Element of EqRelLatt M by MSUALG_5:def 5;
take c;
let a be Element of EqRelLatt M;
reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;
A1: now
let i be object;
A2: ex K1 be ManySortedRelation of M st K1 = c9 (\/) a9 & c9 "\/" a9 =
EqCl K1 by MSUALG_5:def 4;
assume
A3: i in I;
then reconsider i9 = i as Element of I;
reconsider K2 = c9.i9, a2 = a9.i9 as Equivalence_Relation of M.i by
MSUALG_4:def 2;
(c9 (\/) a9).i = c9.i \/ a9.i by A3,PBOOLE:def 4
.= [:M.i,M.i:] \/ a9.i by A3,PBOOLE:def 16
.= nabla M.i \/ a2 by EQREL_1:def 1
.= nabla M.i by EQREL_1:1
.= [:M.i,M.i:] by EQREL_1:def 1
.= c9.i by A3,PBOOLE:def 16;
hence (c9 "\/" a9).i = EqCl K2 by A2,MSUALG_5:def 3
.= c9.i by MSUALG_5:2;
end;
thus c"\/"a = (the L_join of EqRelLatt M).(c,a) by LATTICES:def 1
.= c9 "\/" a9 by MSUALG_5:def 5
.= c by A1,PBOOLE:3;
hence thesis;
end;
then
A4: EqRelLatt M is upper-bounded by LATTICES:def 14;
ex c being Element of EqRelLatt M st for a being Element of EqRelLatt
M holds c"/\"a = c & a"/\"c = c
proof
reconsider c9 = id M as Equivalence_Relation of M by Th1;
reconsider c = c9 as Element of EqRelLatt M by MSUALG_5:def 5;
take c;
let a be Element of EqRelLatt M;
reconsider a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;
A5: now
let i be object;
assume
A6: i in I;
then reconsider i9 = i as Element of I;
reconsider a2 = a9.i9 as Equivalence_Relation of M.i by MSUALG_4:def 2;
thus (c9 (/\) a9).i = c9.i /\ a9.i by A6,PBOOLE:def 5
.= id (M.i) /\ a2 by MSUALG_3:def 1
.= id (M.i) by EQREL_1:10
.= c9.i by A6,MSUALG_3:def 1;
end;
thus c"/\"a = (the L_meet of EqRelLatt M).(c,a) by LATTICES:def 2
.= c9 (/\) a9 by MSUALG_5:def 5
.= c by A5,PBOOLE:3;
hence thesis;
end;
then EqRelLatt M is lower-bounded by LATTICES:def 13;
hence thesis by A4;
end;
end;
theorem
Bottom EqRelLatt M = id M
proof
set K = id M;
K is Equivalence_Relation of M by Th1;
then reconsider K as Element of EqRelLatt M by MSUALG_5:def 5;
now
let a be Element of EqRelLatt M;
reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;
A1: now
let i be object;
assume
A2: i in I;
then reconsider i9 = i as Element of I;
reconsider a2 = a9.i9 as Equivalence_Relation of M.i by MSUALG_4:def 2;
thus (K9 (/\) a9).i = K9.i /\ a9.i by A2,PBOOLE:def 5
.= id (M.i) /\ a2 by MSUALG_3:def 1
.= id (M.i) by EQREL_1:10
.= K9.i by A2,MSUALG_3:def 1;
end;
thus K "/\" a = (the L_meet of EqRelLatt M).(K,a) by LATTICES:def 2
.= K9 (/\) a9 by MSUALG_5:def 5
.= K by A1,PBOOLE:3;
hence a "/\" K = K;
end;
hence thesis by LATTICES:def 16;
end;
theorem
Top EqRelLatt M = [|M,M|]
proof
set K = [|M,M|];
K is Equivalence_Relation of M by Th2;
then reconsider K as Element of EqRelLatt M by MSUALG_5:def 5;
now
let a be Element of EqRelLatt M;
reconsider K9 = K, a9 = a as Equivalence_Relation of M by MSUALG_5:def 5;
A1: now
let i be object;
A2: ex K1 be ManySortedRelation of M st K1 = K9 (\/) a9 & K9 "\/" a9 = EqCl
K1 by MSUALG_5:def 4;
assume
A3: i in I;
then reconsider i9 = i as Element of I;
reconsider K2 = K9.i9, a2 = a9.i9 as Equivalence_Relation of M.i by
MSUALG_4:def 2;
(K9 (\/) a9).i = K9.i \/ a9.i by A3,PBOOLE:def 4
.= [:M.i,M.i:] \/ a9.i by A3,PBOOLE:def 16
.= nabla M.i \/ a2 by EQREL_1:def 1
.= nabla M.i by EQREL_1:1
.= [:M.i,M.i:] by EQREL_1:def 1
.= K9.i by A3,PBOOLE:def 16;
hence (K9 "\/" a9).i = EqCl K2 by A2,MSUALG_5:def 3
.= K9.i by MSUALG_5:2;
end;
thus K "\/" a = (the L_join of EqRelLatt M).(K,a) by LATTICES:def 1
.= K9 "\/" a9 by MSUALG_5:def 5
.= K by A1,PBOOLE:3;
hence a "\/" K = K;
end;
hence thesis by LATTICES:def 17;
end;
theorem Th5:
for X be Subset of EqRelLatt M holds X is SubsetFamily of [|M,M|]
proof
let X be Subset of EqRelLatt M;
now
let x be object;
assume x in the carrier of EqRelLatt M;
then reconsider x9 = x as Equivalence_Relation of M by MSUALG_5:def 5;
now
let i be object;
assume i in I;
then reconsider i9 = i as Element of I;
x9.i9 c= [:M.i9,M.i9:];
hence x9.i c= [|M,M|].i by PBOOLE:def 16;
end;
then x9 c= [|M,M|] by PBOOLE:def 2;
then x9 is ManySortedSubset of [|M,M|] by PBOOLE:def 18;
hence x in Bool [|M,M|] by CLOSURE2:def 1;
end;
then the carrier of EqRelLatt M c= Bool [|M,M|];
then bool the carrier of EqRelLatt M c= bool Bool [|M,M|] by ZFMISC_1:67;
hence thesis;
end;
theorem Th6:
for a,b be Element of EqRelLatt M, A,B be Equivalence_Relation of
M st a = A & b = B holds a [= b iff A c= B
proof
let a,b be Element of EqRelLatt M;
let A,B be Equivalence_Relation of M;
assume that
A1: a = A and
A2: b = B;
thus a [= b implies A c= B
proof
assume
A3: a [= b;
A (/\) B = (the L_meet of EqRelLatt M).(A,B) by MSUALG_5:def 5
.= a "/\" b by A1,A2,LATTICES:def 2
.= A by A1,A3,LATTICES:4;
hence thesis by PBOOLE:15;
end;
thus A c= B implies a [= b
proof
assume
A4: A c= B;
a "/\" b = (the L_meet of EqRelLatt M).(A,B) by A1,A2,LATTICES:def 2
.= A (/\) B by MSUALG_5:def 5
.= a by A1,A4,PBOOLE:23;
hence thesis by LATTICES:4;
end;
end;
theorem Th7:
for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st
X1 = X for a,b be Equivalence_Relation of M st a = meet |:X1:| & b in X holds a
c= b
proof
let X be Subset of EqRelLatt M;
let X1 be SubsetFamily of [|M,M|] such that
A1: X1 = X;
let a,b be Equivalence_Relation of M such that
A2: a = meet |:X1:| and
A3: b in X;
now
reconsider b9 = b as Element of Bool [|M,M|] by A1,A3;
let i be object;
assume
A4: i in I;
then
|:X1:|.i = { x.i where x is Element of Bool [|M,M|] : x in X1 } by A1,A3,
CLOSURE2:14;
then
A5: b9.i in |:X1:|.i by A1,A3;
then
A6: for y being object st y in meet (|:X1:|.i) holds y in b.i
by SETFAM_1:def 1;
ex Q be Subset-Family of ([|M,M|].i) st Q = |:X1:|.i & meet |:X1:|.i =
Intersect Q by A4,MSSUBFAM:def 1;
then a.i = meet (|:X1:|.i) by A2,A5,SETFAM_1:def 9;
hence a.i c= b.i by A6;
end;
hence thesis by PBOOLE:def 2;
end;
theorem Th8:
for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st
X1 = X & X is non empty holds meet |:X1:| is Equivalence_Relation of M
proof
let X be Subset of EqRelLatt M;
let X1 be SubsetFamily of [|M,M|];
set a = meet |:X1:|;
now
let i be set;
assume
A1: i in I;
a c= [|M,M|] by PBOOLE:def 18;
then a.i c= [|M,M|].i by A1,PBOOLE:def 2;
hence a.i is Relation of M.i by A1,PBOOLE:def 16;
end;
then reconsider a as ManySortedRelation of M by MSUALG_4:def 1;
assume that
A2: X1 = X and
A3: X is non empty;
now
reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2,A3;
let i be object, R be Relation of M.i;
assume that
A4: i in I and
A5: a.i = R;
reconsider i9 = i as Element of I by A4;
reconsider b = |:X1:|.i9 as Subset-Family of [:M.i,M.i:] by PBOOLE:def 16;
consider Q be Subset-Family of ([|M,M|].i) such that
A6: Q = |:X1:|.i and
A7: R = Intersect Q by A4,A5,MSSUBFAM:def 1;
reconsider Q as Subset-Family of [:M.i,M.i:] by A4,PBOOLE:def 16;
|:X19:| is non-empty;
then
A8: Q <> {} by A4,A6,PBOOLE:def 13;
A9: |:X19:|.i = { x.i where x is Element of Bool [|M,M|] : x in X1 } by A4,
CLOSURE2:14;
now
let Y;
assume Y in b;
then consider z be Element of Bool [|M,M|] such that
A10: Y = z.i and
A11: z in X by A2,A9;
z c= [|M,M|] by PBOOLE:def 18;
then z.i c= [|M,M|].i by A4,PBOOLE:def 2;
then reconsider Y1 = Y as Relation of M.i by A4,A10,PBOOLE:def 16;
z is Equivalence_Relation of M by A11,MSUALG_5:def 5;
then Y1 is Equivalence_Relation of M.i by A4,A10,MSUALG_4:def 2;
hence Y is Equivalence_Relation of M.i;
end;
then meet b is Equivalence_Relation of M.i by A6,A8,EQREL_1:11;
hence R is Equivalence_Relation of M.i by A6,A7,A8,SETFAM_1:def 9;
end;
hence thesis by MSUALG_4:def 2;
end;
definition
let L be non empty LattStr;
redefine attr L is complete means :: redefines complete (LATTICE3, definition)
for X being Subset of L
ex a being Element of L st X is_less_than a &
for b being Element of L st X is_less_than b holds a [= b;
compatibility
proof
thus L is complete implies for X being Subset of L ex a being Element of L
st X is_less_than a & for b being Element of L st X is_less_than b holds a [= b
;
assume
A1: for X being Subset of L ex a being Element of L st X is_less_than
a & for b being Element of L st X is_less_than b holds a [= b;
let X be set;
defpred P[set] means $1 in X;
set Y = { c where c is Element of L : P[c] };
Y is Subset of L from DOMAIN_1:sch 7;
then consider p being Element of L such that
A2: Y is_less_than p and
A3: for r being Element of L st Y is_less_than r holds p [= r by A1;
take p;
thus X is_less_than p
proof
let q be Element of L;
assume q in X;
then q in Y;
hence thesis by A2;
end;
let r be Element of L;
assume
A4: X is_less_than r;
now
let q be Element of L;
assume q in Y;
then ex v be Element of L st q = v & v in X;
hence q [= r by A4;
end;
then Y is_less_than r;
hence thesis by A3;
end;
end;
theorem Th9:
EqRelLatt M is complete
proof
for X being Subset of EqRelLatt M ex a being Element of EqRelLatt M st a
is_less_than X & for b being Element of EqRelLatt M st b is_less_than X holds b
[= a
proof
let X be Subset of EqRelLatt M;
reconsider X1 = X as SubsetFamily of [|M,M|] by Th5;
per cases;
suppose
A1: X is empty;
take a = Top EqRelLatt M;
for q be Element of EqRelLatt M st q in X holds a [= q by A1;
hence a is_less_than X;
let b be Element of EqRelLatt M;
assume b is_less_than X;
thus thesis by LATTICES:19;
end;
suppose
A2: X is non empty;
then reconsider a = meet |:X1:| as Equivalence_Relation of M by Th8;
set a9 = a;
reconsider a as Element of EqRelLatt M by MSUALG_5:def 5;
take a;
now
let q be Element of EqRelLatt M;
reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def 5;
assume q in X;
then a9 c= q9 by Th7;
hence a [= q by Th6;
end;
hence a is_less_than X;
now
let b be Element of EqRelLatt M;
reconsider b9 = b as Equivalence_Relation of M by MSUALG_5:def 5;
assume
A3: b is_less_than X;
now
reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A2;
let i be object;
assume
A4: i in I;
then
A5: ex Q be Subset-Family of ([|M,M|].i) st Q = |:X1:|.i & meet |:X1
:|.i = Intersect Q by MSSUBFAM:def 1;
|:X19:| is non-empty;
then
A6: |:X1:|.i <> {} by A4,PBOOLE:def 13;
now
let Z be set;
assume
A7: Z in |:X1:|.i;
|:X19:|.i = { x.i where x is Element of Bool [|M,M|] : x in
X1 } by A4,CLOSURE2:14;
then consider z be Element of Bool [|M,M|] such that
A8: Z = z.i and
A9: z in X1 by A7;
reconsider z9 = z as Element of EqRelLatt M by A9;
reconsider z99 = z9 as Equivalence_Relation of M by MSUALG_5:def 5;
b [= z9 by A3,A9;
then b9 c= z99 by Th6;
hence b9.i c= Z by A4,A8,PBOOLE:def 2;
end;
then b9.i c= meet (|:X1:|.i) by A6,SETFAM_1:5;
hence b9.i c= meet |:X1:|.i by A6,A5,SETFAM_1:def 9;
end;
then b9 c= meet |:X1:| by PBOOLE:def 2;
hence b [= a by Th6;
end;
hence thesis;
end;
end;
hence thesis by VECTSP_8:def 6;
end;
registration
let I,M;
cluster EqRelLatt M -> complete;
coherence by Th9;
end;
theorem
for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st X1 =
X & X is non empty for a,b be Equivalence_Relation of M st a = meet |:X1:| & b
= "/\" (X,EqRelLatt M) holds a = b
proof
let X be Subset of EqRelLatt M;
let X1 be SubsetFamily of [|M,M|];
assume that
A1: X1 = X and
A2: X is non empty;
let a,b be Equivalence_Relation of M;
reconsider a9 = a as Element of EqRelLatt M by MSUALG_5:def 5;
assume that
A3: a = meet |:X1:| and
A4: b = "/\" (X,EqRelLatt M);
A5: now
reconsider X19 = X1 as non empty SubsetFamily of [|M,M|] by A1,A2;
let c be Element of EqRelLatt M;
reconsider c9 = c as Equivalence_Relation of M by MSUALG_5:def 5;
reconsider S = |:X19:| as non-empty MSSubsetFamily of [|M,M|];
assume
A6: c is_less_than X;
now
let Z1 be ManySortedSet of I;
assume
A7: Z1 in S;
now
let i be object;
assume
A8: i in I;
then
Z1.i in |:X1:|.i & |:X19:|.i = { x1.i where x1 is Element of Bool
[|M,M|] : x1 in X1 } by A7,CLOSURE2:14,PBOOLE:def 1;
then consider z be Element of Bool [|M,M|] such that
A9: Z1.i = z.i and
A10: z in X1;
reconsider z9 = z as Element of EqRelLatt M by A1,A10;
reconsider z1 = z9 as Equivalence_Relation of M by MSUALG_5:def 5;
c [= z9 by A1,A6,A10;
then c9 c= z1 by Th6;
hence c9.i c= Z1.i by A8,A9,PBOOLE:def 2;
end;
hence c9 c= Z1 by PBOOLE:def 2;
end;
then c9 c= meet |:X1:| by MSSUBFAM:45;
hence c [= a9 by A3,Th6;
end;
now
let q be Element of EqRelLatt M;
reconsider q9 = q as Equivalence_Relation of M by MSUALG_5:def 5;
assume q in X;
then a c= q9 by A1,A3,Th7;
hence a9 [= q by Th6;
end;
then a9 is_less_than X;
hence thesis by A4,A5,LATTICE3:34;
end;
begin :: SUBLATTICES INHERITING SUP'S AND INF'S
definition
let L be Lattice;
let IT be SubLattice of L;
attr IT is /\-inheriting means
for X being Subset of IT holds "/\" (X ,L) in the carrier of IT;
attr IT is \/-inheriting means
for X being Subset of IT holds "\/" (X ,L) in the carrier of IT;
end;
theorem Th11:
for L be Lattice, L9 be SubLattice of L, a,b be Element of L, a9
,b9 be Element of L9 st a = a9 & b = b9 holds a "\/" b = a9 "\/" b9 & a "/\" b
= a9 "/\" b9
proof
let L be Lattice;
let L9 be SubLattice of L;
let a,b be Element of L;
let a9,b9 be Element of L9;
assume
A1: a = a9 & b = b9;
thus a "\/" b = (the L_join of L).(a,b) by LATTICES:def 1
.= ((the L_join of L)||the carrier of L9). [a9,b9] by A1,FUNCT_1:49
.= (the L_join of L9).(a9,b9) by NAT_LAT:def 12
.= a9 "\/" b9 by LATTICES:def 1;
thus a "/\" b = (the L_meet of L).(a,b) by LATTICES:def 2
.= ((the L_meet of L)||the carrier of L9). [a9,b9] by A1,FUNCT_1:49
.= (the L_meet of L9).(a9,b9) by NAT_LAT:def 12
.= a9 "/\" b9 by LATTICES:def 2;
end;
theorem Th12:
for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be
Element of L, a9 be Element of L9 st a = a9 holds a is_less_than X iff a9
is_less_than X
proof
let L be Lattice;
let L9 be SubLattice of L;
let X be Subset of L9;
let a be Element of L;
let a9 be Element of L9;
assume
A1: a = a9;
thus a is_less_than X implies a9 is_less_than X
proof
assume
A2: a is_less_than X;
now
let q9 be Element of L9;
the carrier of L9 c= the carrier of L by NAT_LAT:def 12;
then reconsider q = q9 as Element of L;
assume q9 in X;
then
A3: a [= q by A2;
a9 "/\" q9 = a "/\" q by A1,Th11
.= a9 by A1,A3,LATTICES:4;
hence a9 [= q9 by LATTICES:4;
end;
hence thesis;
end;
thus a9 is_less_than X implies a is_less_than X
proof
assume
A4: a9 is_less_than X;
now
let q be Element of L;
assume
A5: q in X;
then reconsider q9 = q as Element of L9;
A6: a9 [= q9 by A4,A5;
a "/\" q = a9 "/\" q9 by A1,Th11
.= a by A1,A6,LATTICES:4;
hence a [= q by LATTICES:4;
end;
hence thesis;
end;
end;
theorem Th13:
for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be
Element of L, a9 be Element of L9 st a = a9 holds X is_less_than a iff X
is_less_than a9
proof
let L be Lattice;
let L9 be SubLattice of L;
let X be Subset of L9;
let a be Element of L;
let a9 be Element of L9;
assume
A1: a = a9;
thus X is_less_than a implies X is_less_than a9
proof
assume
A2: X is_less_than a;
now
let q9 be Element of L9;
the carrier of L9 c= the carrier of L by NAT_LAT:def 12;
then reconsider q = q9 as Element of L;
assume q9 in X;
then
A3: q [= a by A2;
q9 "/\" a9 = q "/\" a by A1,Th11
.= q9 by A3,LATTICES:4;
hence q9 [= a9 by LATTICES:4;
end;
hence thesis;
end;
thus X is_less_than a9 implies X is_less_than a
proof
assume
A4: X is_less_than a9;
now
let q be Element of L;
assume
A5: q in X;
then reconsider q9 = q as Element of L9;
A6: q9 [= a9 by A4,A5;
q "/\" a = q9 "/\" a9 by A1,Th11
.= q by A6,LATTICES:4;
hence q [= a by LATTICES:4;
end;
hence thesis;
end;
end;
theorem Th14:
for L be complete Lattice, L9 be SubLattice of L st L9 is
/\-inheriting holds L9 is complete
proof
let L be complete Lattice;
let L9 be SubLattice of L such that
A1: L9 is /\-inheriting;
for X being Subset of L9 ex a being Element of L9 st a is_less_than X &
for b being Element of L9 st b is_less_than X holds b [= a
proof
let X be Subset of L9;
set a = "/\" (X,L);
reconsider a9 = a as Element of L9 by A1;
take a9;
a is_less_than X by LATTICE3:34;
hence a9 is_less_than X by Th12;
let b9 be Element of L9;
the carrier of L9 c= the carrier of L by NAT_LAT:def 12;
then reconsider b = b9 as Element of L;
assume b9 is_less_than X;
then b is_less_than X by Th12;
then
A2: b [= a by LATTICE3:39;
b9 "/\" a9 = b "/\" a by Th11
.= b9 by A2,LATTICES:4;
hence thesis by LATTICES:4;
end;
hence thesis by VECTSP_8:def 6;
end;
theorem Th15:
for L be complete Lattice, L9 be SubLattice of L st L9 is
\/-inheriting holds L9 is complete
proof
let L be complete Lattice;
let L9 be SubLattice of L such that
A1: L9 is \/-inheriting;
for X being Subset of L9 ex a being Element of L9 st X is_less_than a &
for b being Element of L9 st X is_less_than b holds a [= b
proof
let X be Subset of L9;
set a = "\/" (X,L);
reconsider a9 = a as Element of L9 by A1;
take a9;
X is_less_than a by LATTICE3:def 21;
hence X is_less_than a9 by Th13;
let b9 be Element of L9;
the carrier of L9 c= the carrier of L by NAT_LAT:def 12;
then reconsider b = b9 as Element of L;
assume X is_less_than b9;
then X is_less_than b by Th13;
then
A2: a [= b by LATTICE3:def 21;
a9 "/\" b9 = a "/\" b by Th11
.= a9 by A2,LATTICES:4;
hence thesis by LATTICES:4;
end;
hence thesis;
end;
registration
let L be complete Lattice;
cluster complete for SubLattice of L;
existence
proof
reconsider L1 = L as SubLattice of L by NAT_LAT:15;
take L1;
thus thesis;
end;
end;
registration
let L be complete Lattice;
cluster /\-inheriting -> complete for SubLattice of L;
coherence by Th14;
cluster \/-inheriting -> complete for SubLattice of L;
coherence by Th15;
end;
theorem Th16:
for L be complete Lattice, L9 be SubLattice of L st L9 is
/\-inheriting for A9 be Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9)
proof
let L be complete Lattice;
let L9 be SubLattice of L;
assume
A1: L9 is /\-inheriting;
then reconsider L91 = L9 as complete SubLattice of L;
let A9 be Subset of L9;
set a = "/\" (A9,L);
reconsider a9 = a as Element of L91 by A1;
A2: now
let c9 be Element of L91;
the carrier of L91 c= the carrier of L by NAT_LAT:def 12;
then reconsider c = c9 as Element of L;
assume c9 is_less_than A9;
then c is_less_than A9 by Th12;
then
A3: c [= a by LATTICE3:34;
c9 "/\" a9 = c "/\" a by Th11
.= c9 by A3,LATTICES:4;
hence c9 [= a9 by LATTICES:4;
end;
a is_less_than A9 by LATTICE3:34;
then a9 is_less_than A9 by Th12;
hence thesis by A2,LATTICE3:34;
end;
theorem Th17:
for L be complete Lattice, L9 be SubLattice of L st L9 is
\/-inheriting for A9 be Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)
proof
let L be complete Lattice;
let L9 be SubLattice of L;
assume
A1: L9 is \/-inheriting;
then reconsider L91 = L9 as complete SubLattice of L;
let A9 be Subset of L9;
set a = "\/" (A9,L);
reconsider a9 = a as Element of L91 by A1;
A2: now
let c9 be Element of L91;
the carrier of L91 c= the carrier of L by NAT_LAT:def 12;
then reconsider c = c9 as Element of L;
assume A9 is_less_than c9;
then A9 is_less_than c by Th13;
then
A3: a [= c by LATTICE3:def 21;
a9 "/\" c9 = a "/\" c by Th11
.= a9 by A3,LATTICES:4;
hence a9 [= c9 by LATTICES:4;
end;
A9 is_less_than a by LATTICE3:def 21;
then A9 is_less_than a9 by Th13;
hence thesis by A2,LATTICE3:def 21;
end;
theorem
for L be complete Lattice, L9 be SubLattice of L st L9 is
/\-inheriting for A be Subset of L, A9 be Subset of L9 st A = A9 holds "/\" A =
"/\" A9 by Th16;
theorem
for L be complete Lattice, L9 be SubLattice of L st L9 is
\/-inheriting for A be Subset of L, A9 be Subset of L9 st A = A9 holds "\/" A =
"\/" A9 by Th17;
begin :: SEGMENT OF REAL NUMBERS AS A COMPLETE LATTICE
definition
let r1,r2 such that
A1: r1 <= r2;
func RealSubLatt(r1,r2) -> strict Lattice means
:Def4:
the carrier of it =
[.r1,r2.] & the L_join of it = maxreal||[.r1,r2.] & the L_meet of it = minreal
||[.r1,r2.];
existence
proof
r2 in { r : r1 <= r & r <= r2 } by A1;
then reconsider A = [.r1,r2.] as non empty set by RCOMP_1:def 1;
[:A,A:] c= [:REAL,REAL:] by ZFMISC_1:96;
then reconsider
Ma = maxreal||A, Mi = minreal||A as Function of [:A,A:],REAL by FUNCT_2:32;
A2: dom Mi = [:A,A:] by FUNCT_2:def 1;
A3: now
let x be object;
assume
A4: x in dom Mi;
then consider x1,x2 be object such that
A5: x = [x1,x2] by RELAT_1:def 1;
x2 in A by A4,A5,ZFMISC_1:87;
then x2 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;
then consider y2 be Real such that
A6: x2 = y2 and
A7: r1 <= y2 & y2 <= r2;
reconsider y2 as Real;
x1 in A by A4,A5,ZFMISC_1:87;
then x1 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;
then consider y1 be Real such that
A8: x1 = y1 and
A9: r1 <= y1 & y1 <= r2;
reconsider y1 as Real;
Mi.x = minreal.(x1,x2) by A4,A5,FUNCT_1:49
.= min(y1,y2) by A8,A6,REAL_LAT:def 1;
then Mi.x = y1 or Mi.x = y2 by XXREAL_0:15;
then Mi.x in { r : r1 <= r & r <= r2 } by A9,A7;
hence Mi.x in A by RCOMP_1:def 1;
end;
A10: now
let x be object;
assume
A11: x in dom Ma;
then consider x1,x2 be object such that
A12: x = [x1,x2] by RELAT_1:def 1;
x2 in A by A11,A12,ZFMISC_1:87;
then x2 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;
then consider y2 be Real such that
A13: x2 = y2 and
A14: r1 <= y2 & y2 <= r2;
reconsider y2 as Real;
x1 in A by A11,A12,ZFMISC_1:87;
then x1 in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;
then consider y1 be Real such that
A15: x1 = y1 and
A16: r1 <= y1 & y1 <= r2;
reconsider y1 as Real;
Ma.x = maxreal.(x1,x2) by A11,A12,FUNCT_1:49
.= max(y1,y2) by A15,A13,REAL_LAT:def 2;
then Ma.x = y1 or Ma.x = y2 by XXREAL_0:16;
then Ma.x in { r : r1 <= r & r <= r2 } by A16,A14;
hence Ma.x in A by RCOMP_1:def 1;
end;
reconsider Mi as BinOp of A by A2,A3,FUNCT_2:3;
dom Ma = [:A,A:] by FUNCT_2:def 1;
then reconsider Ma as BinOp of A by A10,FUNCT_2:3;
set R = Real_Lattice;
set L9 = LattStr (# A, Ma, Mi #);
reconsider L = L9 as non empty LattStr;
A17: now
let a,b be Element of L;
thus a"\/"b = (the L_join of L).(a,b) by LATTICES:def 1
.= maxreal. [a,b] by FUNCT_1:49
.= maxreal.(a,b);
thus a"/\"b = (the L_meet of L).(a,b) by LATTICES:def 2
.= minreal. [a,b] by FUNCT_1:49
.= minreal.(a,b);
end;
A18: for x being Element of A holds x is Element of R
by REAL_LAT:def 3,XREAL_0:def 1;
A19: now
let p,q be Element of L;
reconsider p9 = p, q9 = q as Element of R by A18;
thus p"\/"q = maxreal.(p,q) by A17
.= maxreal.(q9,p9) by REAL_LAT:1
.= q"\/"p by A17;
end;
A20: now
let p,q be Element of L;
reconsider p9 = p, q9 = q as Element of R by A18;
thus p"/\"(p"\/"q) = minreal.(p,p"\/"q) by A17
.= minreal.(p9,maxreal.(p9,q9)) by A17
.= p by REAL_LAT:6;
end;
A21: now
let p,q be Element of L;
reconsider p9 = p, q9 = q as Element of R by A18;
thus p"/\"q = minreal.(p,q) by A17
.= minreal.(q9,p9) by REAL_LAT:2
.= q"/\"p by A17;
end;
A22: now
let p,q be Element of L;
reconsider p9 = p, q9 = q as Element of R by A18;
thus (p"/\"q)"\/"q = maxreal.(p"/\"q,q) by A17
.= maxreal.(minreal.(p9,q9),q9) by A17
.= q by REAL_LAT:5;
end;
A23: now
let p,q,r be Element of L;
reconsider p9 = p, q9 = q, r9 = r as Element of R by A18;
thus p"/\"(q"/\"r) = minreal.(p,q"/\"r) by A17
.= minreal.(p,minreal.(q,r)) by A17
.= minreal.(minreal.(p9,q9),r9) by REAL_LAT:4
.= minreal.(p"/\"q,r) by A17
.= (p"/\"q)"/\"r by A17;
end;
now
let p,q,r be Element of L;
reconsider p9 = p, q9 = q, r9 = r as Element of R by A18;
thus p"\/"(q"\/"r) = maxreal.(p,q"\/"r) by A17
.= maxreal.(p,maxreal.(q,r)) by A17
.= maxreal.(maxreal.(p9,q9),r9) by REAL_LAT:3
.= maxreal.(p"\/"q,r) by A17
.= (p"\/"q)"\/"r by A17;
end;
then L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A19,A22,A21,A23,A20,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
then reconsider L9 as strict Lattice;
take L9;
thus thesis;
end;
uniqueness;
end;
theorem Th20:
for r1,r2 st r1 <= r2 holds RealSubLatt(r1,r2) is complete
proof
let r1,r2 such that
A1: r1 <= r2;
reconsider R1 = r1, R2 = r2 as R_eal by XXREAL_0:def 1;
set A = [.r1,r2.];
set L9 = RealSubLatt(r1,r2);
A2: the carrier of L9 = [.r1,r2.] by A1,Def4;
A3: the L_meet of L9 = minreal||[.r1,r2.] by A1,Def4;
now
let X be Subset of L9;
per cases;
suppose
A4: X is empty;
thus ex a be Element of L9 st a is_less_than X & for b being Element of
L9 st b is_less_than X holds b [= a
proof
r2 in { r : r1 <= r & r <= r2 } by A1;
then reconsider a = r2 as Element of L9 by A2,RCOMP_1:def 1;
take a;
for q be Element of L9 st q in X holds a [= q by A4;
hence a is_less_than X;
let b be Element of L9;
assume b is_less_than X;
A5: b in [.r1,r2.] by A2;
then reconsider b9 = b as Element of REAL;
b in { r : r1 <= r & r <= r2 } by A5,RCOMP_1:def 1;
then consider b1 be Real such that
A6: b = b1 & r1 <= b1 & b1 <= r2;
reconsider b1,r2 as Real;
b "/\" a = (minreal||A).(b,a) by A3,LATTICES:def 2
.= minreal. [b,a] by A2,FUNCT_1:49
.= minreal.(b,a)
.= min(b9,r2) by REAL_LAT:def 1
.= b by A6,XXREAL_0:def 9;
hence thesis by LATTICES:4;
end;
end;
suppose
A7: X is non empty;
X c= REAL by A2,XBOOLE_1:1;
then reconsider X1 = X as non empty Subset of ExtREAL by A7,NUMBERS:31
,XBOOLE_1:1;
thus ex a be Element of L9 st a is_less_than X & for b being Element of
L9 st b is_less_than X holds b [= a
proof
set g = the Element of X1;
set A1 = inf X1;
set LB = r1 - 1;
LB is LowerBound of X1
proof
let v be ExtReal;
assume v in X1;
then v in the carrier of L9;
then v in { r : r1 <= r & r <= r2 } by A2,RCOMP_1:def 1;
then consider w be Real such that
A8: v = w and
A9: r1 <= w and
w <= r2;
r1 - 1 <= r1 - 0 by XREAL_1:13;
then r1 - 1 + r1 <= r1 + w by A9,XREAL_1:7;
hence LB <= v by A8,XREAL_1:6;
end;
then
A10: X1 is bounded_below;
X <> {+infty}
proof
assume X = {+infty};
then +infty in X by TARSKI:def 1;
hence contradiction by A2;
end;
then
A11: A1 in REAL by A10,XXREAL_2:58;
g in [.r1,r2.] by A2,TARSKI:def 3;
then g in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;
then
A12: ex w be Real st g = w & r1 <= w & w <= r2;
A13: A1 is LowerBound of X1 by XXREAL_2:def 4;
then A1 <= g by XXREAL_2:def 2;
then consider A9,R29 be Real such that
A14: A9 = A1 and
A15: R29 = R2 & A9 <= R29 by A11,A12,XXREAL_0:2;
now
let v be ExtReal;
assume v in X1;
then v in A by A2;
then v in { r : r1 <= r & r <= r2 } by RCOMP_1:def 1;
then ex w be Real st v = w & r1 <= w & w <= r2;
hence R1 <= v;
end;
then R1 is LowerBound of X1 by XXREAL_2:def 2;
then R1 <= A1 by XXREAL_2:def 4;
then A9 in { r : r1 <= r & r <= r2 } by A14,A15;
then reconsider a = A1 as Element of L9 by A2,A14,RCOMP_1:def 1;
take a;
a in [.r1,r2.] by A2;
then reconsider a9 = a as Element of REAL;
now
let q be Element of L9;
assume
A16: q in X;
q in [.r1,r2.] by A2;
then reconsider q9 = q as Element of REAL;
reconsider Q = q9 as R_eal by NUMBERS:31;
A1 = a9;
then
A17: ex a1, q1 be Real st a1 = A1 & q1 = Q & a1 <= q1 by A13,A16,
XXREAL_2:def 2;
a "/\" q = (minreal||A).(a,q) by A3,LATTICES:def 2
.= minreal. [a,q] by A2,FUNCT_1:49
.= minreal.(a,q)
.= min(a9,q9) by REAL_LAT:def 1
.= a by A17,XXREAL_0:def 9;
hence a [= q by LATTICES:4;
end;
hence a is_less_than X;
let b be Element of L9;
b in [.r1,r2.] by A2;
then reconsider b9 = b as Element of REAL;
reconsider B = b9 as R_eal by NUMBERS:31;
assume
A18: b is_less_than X;
now
let h be ExtReal;
assume
A19: h in X;
then reconsider h1 = h as Element of L9;
h in [.r1,r2.] by A2,A19;
then reconsider h9 = h as Real;
A20: b [= h1 by A18,A19;
min(b9,h9) = minreal.(b,h1) by REAL_LAT:def 1
.= (minreal||A). [b,h1] by A2,FUNCT_1:49
.= (minreal||A).(b,h1)
.= b "/\" h1 by A3,LATTICES:def 2
.= b9 by A20,LATTICES:4;
hence B <= h by XXREAL_0:def 9;
end;
then B is LowerBound of X1 by XXREAL_2:def 2;
then
A21: B <= A1 by XXREAL_2:def 4;
b "/\" a = (minreal||A).(b,a) by A3,LATTICES:def 2
.= minreal. [b,a] by A2,FUNCT_1:49
.= minreal.(b,a)
.= min(b9,a9) by REAL_LAT:def 1
.= b by A21,XXREAL_0:def 9;
hence thesis by LATTICES:4;
end;
end;
end;
hence thesis by VECTSP_8:def 6;
end;
reconsider jj=1 as Real;
reconsider jd=1/2 as Real;
theorem Th21:
ex L9 be SubLattice of RealSubLatt(In(0,REAL),In(1,REAL))
st L9 is \/-inheriting
non /\-inheriting
proof
set B = {0,1} \/ ].1/2,1.[;
set L = RealSubLatt(In(0,REAL),In(1,REAL));
set R = Real_Lattice;
A1: B c= {0} \/ { x where x is Real: 1/2 < x & x <= 1 }
proof
let x1 be object;
assume
A2: x1 in B;
now
per cases by A2,XBOOLE_0:def 3;
suppose
x1 in {0,1};
then x1 = 0 or x1 = 1 by TARSKI:def 2;
then x1 in {0} or x1 in { x where x is Real: 1/2 < x & x
<= jj } by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x1 in ].1/2,1.[;
then x1 in { r : 1/2 < r & r < 1 } by RCOMP_1:def 2;
then consider y be Real such that
A3: x1 = y and
A4: 1/2 < y & y < 1;
y in { x where x is Real : 1/2 < x & x <= 1 } by A4;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
{0} \/ { x where x is Real : 1/2 < x & x <= 1 } c= B
proof
let x1 be object;
assume
A5: x1 in {0} \/ { x where x is Real : 1/2 < x & x <= 1 };
now
per cases by A5,XBOOLE_0:def 3;
suppose
x1 in {0};
then x1 = 0 by TARSKI:def 1;
then x1 in {0,1} by TARSKI:def 2;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x1 in { x where x is Real : 1/2 < x & x <= 1 };
then consider y be Real such that
A6: x1 = y and
A7: 1/2 < y and
A8: y <= 1;
y < 1 or y = 1 by A8,XXREAL_0:1;
then y in { r : 1/2 < r & r < 1 } or y = 1 by A7;
then y in ].1/2,1.[ or y in {0,1} by RCOMP_1:def 2,TARSKI:def 2;
hence thesis by A6,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
then
A9: B = {0} \/ { x where x is Real : 1/2 < x & x <= 1 } by A1,
XBOOLE_0:def 10;
A10: 0 in { r : 0 <= r & r <= 1 };
then reconsider A = [.0,jj.] as non empty set by RCOMP_1:def 1;
A11: the L_meet of L = minreal||[.0,jj.] by Def4;
reconsider B as non empty set;
A12: the L_join of L = maxreal||[.0,jj.] by Def4;
A13: A = the carrier of L by Def4;
then reconsider Ma = maxreal||A, Mi = minreal||A as BinOp of A by Def4;
A14: now
let x1 be object;
assume
A15: x1 in B;
now
per cases by A1,A15,XBOOLE_0:def 3;
suppose
x1 in {0};
then x1 = 0 by TARSKI:def 1;
hence x1 in A by A10,RCOMP_1:def 1;
end;
suppose
x1 in { x where x is Real: 1/2 < x & x <= 1 };
then ex y be Real st x1 = y & 1/2 < y & y <= 1;
then x1 in { r : 0 <= r & r <= 1 };
hence x1 in A by RCOMP_1:def 1;
end;
end;
hence x1 in A;
end;
then
A16: B c= A;
then
A17: [:B,B:] c= [:A,A:] by ZFMISC_1:96;
then reconsider ma = Ma||B, mi = Mi||B as Function of [:B,B:],A by FUNCT_2:32
;
A18: for x1 being Element of A holds x1 is Element of R
by REAL_LAT:def 3,XREAL_0:def 1;
A19: dom mi = [:B,B:] by FUNCT_2:def 1;
A20: now
let x9 be object;
assume
A21: x9 in dom mi;
then consider x1,x2 be object such that
A22: x9 = [x1,x2] by RELAT_1:def 1;
A23: x2 in B by A21,A22,ZFMISC_1:87;
A24: x1 in B by A21,A22,ZFMISC_1:87;
now
per cases by A1,A24,XBOOLE_0:def 3;
suppose
x1 in {0};
then
A25: x1 = 0 by TARSKI:def 1;
now
per cases by A1,A23,XBOOLE_0:def 3;
suppose
x2 in {0};
then
A26: x2 = 0 by TARSKI:def 1;
mi.x9 = Mi. [x1,x2] by A21,A22,FUNCT_1:49
.= minreal.(x1,x2) by A17,A21,A22,FUNCT_1:49
.= min(0,0) by A25,A26,REAL_LAT:def 1
.= 0;
then mi.x9 in {0} by TARSKI:def 1;
hence mi.x9 in B by A9,XBOOLE_0:def 3;
end;
suppose
x2 in { x where x is Real : 1/2 < x & x <= 1 };
then consider y2 be Real such that
A27: x2 = y2 and
A28: 1/2 < y2 & y2 <= 1;
reconsider y2 as Real;
mi.x9 = Mi. [x1,x2] by A21,A22,FUNCT_1:49
.= minreal.(x1,x2) by A17,A21,A22,FUNCT_1:49
.= min(0,y2) by A25,A27,REAL_LAT:def 1;
then mi.x9 = 0 or mi.x9 = y2 by XXREAL_0:15;
then
mi.x9 in {0} or mi.x9 in { x where x is Real : 1/2
< x & x <= 1 } by A28,TARSKI:def 1;
hence mi.x9 in B by A9,XBOOLE_0:def 3;
end;
end;
hence mi.x9 in B;
end;
suppose
x1 in { x where x is Real : 1/2 < x & x <= 1 };
then consider y1 be Real such that
A29: x1 = y1 and
A30: 1/2 < y1 & y1 <= 1;
reconsider y1 as Real;
now
per cases by A1,A23,XBOOLE_0:def 3;
suppose
x2 in {0};
then
A31: x2 = 0 by TARSKI:def 1;
mi.x9 = Mi. [x1,x2] by A21,A22,FUNCT_1:49
.= minreal.(x1,x2) by A17,A21,A22,FUNCT_1:49
.= min(y1,0) by A29,A31,REAL_LAT:def 1;
then mi.x9 = y1 or mi.x9 = 0 by XXREAL_0:15;
then mi.x9 in { x where x is Real : 1/2 < x & x <= 1 }
or mi.x9 in {0} by A30,TARSKI:def 1;
hence mi.x9 in B by A9,XBOOLE_0:def 3;
end;
suppose
x2 in { x where x is Real : 1/2 < x & x <= 1 };
then consider y2 be Real such that
A32: x2 = y2 and
A33: 1/2 < y2 & y2 <= 1;
reconsider y2 as Real;
mi.x9 = Mi. [x1,x2] by A21,A22,FUNCT_1:49
.= minreal.(x1,x2) by A17,A21,A22,FUNCT_1:49
.= min(y1,y2) by A29,A32,REAL_LAT:def 1;
then mi.x9 = y1 or mi.x9 = y2 by XXREAL_0:15;
then mi.x9 in { x where x is Real : 1/2 < x & x <= 1 }
by A30,A33;
hence mi.x9 in B by A9,XBOOLE_0:def 3;
end;
end;
hence mi.x9 in B;
end;
end;
hence mi.x9 in B;
end;
A34: dom ma = [:B,B:] by FUNCT_2:def 1;
A35: now
let x9 be object;
assume
A36: x9 in dom ma;
then consider x1,x2 be object such that
A37: x9 = [x1,x2] by RELAT_1:def 1;
A38: x2 in B by A36,A37,ZFMISC_1:87;
A39: x1 in B by A36,A37,ZFMISC_1:87;
now
per cases by A1,A39,XBOOLE_0:def 3;
suppose
x1 in {0};
then
A40: x1 = 0 by TARSKI:def 1;
now
per cases by A1,A38,XBOOLE_0:def 3;
suppose
x2 in {0};
then
A41: x2 = 0 by TARSKI:def 1;
ma.x9 = Ma. [x1,x2] by A36,A37,FUNCT_1:49
.= maxreal.(x1,x2) by A17,A36,A37,FUNCT_1:49
.= max(0,0) by A40,A41,REAL_LAT:def 2
.= 0;
then ma.x9 in {0} by TARSKI:def 1;
hence ma.x9 in B by A9,XBOOLE_0:def 3;
end;
suppose
x2 in { x where x is Real : 1/2 < x & x <= 1 };
then consider y2 be Real such that
A42: x2 = y2 and
A43: 1/2 < y2 & y2 <= 1;
reconsider y2 as Real;
ma.x9 = Ma. [x1,x2] by A36,A37,FUNCT_1:49
.= maxreal.(x1,x2) by A17,A36,A37,FUNCT_1:49
.= max(0,y2) by A40,A42,REAL_LAT:def 2;
then ma.x9 = 0 or ma.x9 = y2 by XXREAL_0:16;
then
ma.x9 in {0} or ma.x9 in { x where x is Real : 1/2
< x & x <= 1 } by A43,TARSKI:def 1;
hence ma.x9 in B by A9,XBOOLE_0:def 3;
end;
end;
hence ma.x9 in B;
end;
suppose
x1 in { x where x is Real : 1/2 < x & x <= 1 };
then consider y1 be Real such that
A44: x1 = y1 and
A45: 1/2 < y1 & y1 <= 1;
reconsider y1 as Real;
now
per cases by A1,A38,XBOOLE_0:def 3;
suppose
x2 in {0};
then
A46: x2 = 0 by TARSKI:def 1;
ma.x9 = Ma. [x1,x2] by A36,A37,FUNCT_1:49
.= maxreal.(x1,x2) by A17,A36,A37,FUNCT_1:49
.= max(y1,0) by A44,A46,REAL_LAT:def 2;
then ma.x9 = y1 or ma.x9 = 0 by XXREAL_0:16;
then ma.x9 in { x where x is Real: 1/2 < x & x <= 1 }
or ma.x9 in {0} by A45,TARSKI:def 1;
hence ma.x9 in B by A9,XBOOLE_0:def 3;
end;
suppose
x2 in { x where x is Real : 1/2 < x & x <= 1 };
then consider y2 be Real such that
A47: x2 = y2 and
A48: 1/2 < y2 & y2 <= 1;
reconsider y2 as Real;
ma.x9 = Ma. [x1,x2] by A36,A37,FUNCT_1:49
.= maxreal.(x1,x2) by A17,A36,A37,FUNCT_1:49
.= max(y1,y2) by A44,A47,REAL_LAT:def 2;
then ma.x9 = y1 or ma.x9 = y2 by XXREAL_0:16;
then ma.x9 in { x where x is Real: 1/2 < x & x <= 1 }
by A45,A48;
hence ma.x9 in B by A9,XBOOLE_0:def 3;
end;
end;
hence ma.x9 in B;
end;
end;
hence ma.x9 in B;
end;
reconsider mi as BinOp of B by A19,A20,FUNCT_2:3;
reconsider ma as BinOp of B by A34,A35,FUNCT_2:3;
reconsider L9 = LattStr (# B, ma, mi #) as non empty LattStr;
A49: now
let a,b be Element of L9;
thus a"\/"b = (the L_join of L9).(a,b) by LATTICES:def 1
.= (maxreal||A). [a,b] by FUNCT_1:49
.= maxreal.(a,b) by A17,FUNCT_1:49;
thus a"/\"b = (the L_meet of L9).(a,b) by LATTICES:def 2
.= (minreal||A). [a,b] by FUNCT_1:49
.= minreal.(a,b) by A17,FUNCT_1:49;
end;
reconsider L as complete Lattice by Th20;
A50: now
let x1 be Element of B;
now
per cases by A9,XBOOLE_0:def 3;
suppose
x1 in {0};
then x1 = 0 by TARSKI:def 1;
hence x1 is Element of L by A10,A13,RCOMP_1:def 1;
end;
suppose
x1 in { x where x is Real : 1/2 < x & x <= 1 };
then ex y be Real st x1 = y & 1/2 < y & y <= 1;
then x1 in { r : 0 <= r & r <= 1 };
hence x1 is Element of L by A13,RCOMP_1:def 1;
end;
end;
hence x1 is Element of L;
end;
A51: now
let p,q be Element of L9;
reconsider p9 = p, q9 = q as Element of L by A50;
reconsider p9, q9 as Element of R by A13,A18;
thus p"\/"q = maxreal.(p,q) by A49
.= maxreal.(q9,p9) by REAL_LAT:1
.= q"\/"p by A49;
end;
A52: now
let p,q be Element of L9;
reconsider p9 = p, q9 = q as Element of L by A50;
reconsider p9, q9 as Element of R by A13,A18;
thus p"/\"(p"\/"q) = minreal.(p,p"\/"q) by A49
.= minreal.(p9,maxreal.(p9,q9)) by A49
.= p by REAL_LAT:6;
end;
A53: now
let p,q be Element of L9;
reconsider p9 = p, q9 = q as Element of L by A50;
reconsider p9, q9 as Element of R by A13,A18;
thus p"/\"q = minreal.(p,q) by A49
.= minreal.(q9,p9) by REAL_LAT:2
.= q"/\"p by A49;
end;
A54: now
let p,q be Element of L9;
reconsider p9 = p, q9 = q as Element of L by A50;
reconsider p9, q9 as Element of R by A13,A18;
thus (p"/\"q)"\/"q = maxreal.(p"/\"q,q) by A49
.= maxreal.(minreal.(p9,q9),q9) by A49
.= q by REAL_LAT:5;
end;
A55: now
let p,q,r be Element of L9;
reconsider p9 = p, q9 = q, r9 = r as Element of L by A50;
reconsider p9, q9, r9 as Element of R by A13,A18;
thus p"/\"(q"/\"r) = minreal.(p,q"/\"r) by A49
.= minreal.(p,minreal.(q,r)) by A49
.= minreal.(minreal.(p9,q9),r9) by REAL_LAT:4
.= minreal.(p"/\"q,r) by A49
.= (p"/\"q)"/\"r by A49;
end;
now
let p,q,r be Element of L9;
reconsider p9 = p, q9 = q, r9 = r as Element of L by A50;
reconsider p9, q9, r9 as Element of R by A13,A18;
thus p"\/"(q"\/"r) = maxreal.(p,q"\/"r) by A49
.= maxreal.(p,maxreal.(q,r)) by A49
.= maxreal.(maxreal.(p9,q9),r9) by REAL_LAT:3
.= maxreal.(p"\/"q,r) by A49
.= (p"\/"q)"\/"r by A49;
end;
then L9 is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A51,A54,A53,A55,A52,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
then reconsider L9 as Lattice;
reconsider L9 as SubLattice of
RealSubLatt(In(0,REAL),In(1,REAL)) by A13,A12,A11,A16,
NAT_LAT:def 12;
take L9;
now
let X be Subset of L9;
thus "\/" (X,L) in the carrier of L9
proof
0 in { r : 0 <= r & r <= 1 };
then reconsider w = 0 as Element of L by A13,RCOMP_1:def 1;
A56: X is_less_than "\/" (X,L) by LATTICE3:def 21;
"\/" (X,L) in [.0,1.] by A13;
then "\/" (X,L) in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;
then consider y be Real such that
A57: y = "\/" (X,L) and
0 <= y and
A58: y <= 1;
reconsider y as Real;
assume
A59: not "\/" (X,L) in the carrier of L9;
then not "\/" (X,L) in { x where x is Real : 1/2 < x & x <=
1 } by A9,XBOOLE_0:def 3;
then
A60: y <= 1/2 by A57,A58;
now
let z9 be object;
assume
A61: z9 in X;
then reconsider z = z9 as Element of L9;
reconsider z as Element of L by A13,A14;
A62: z [= "\/" (X,L) by A56,A61;
reconsider z1 = z as Real;
reconsider z1 as Real;
min(z1,y) = minreal.(z1,"\/" (X,L)) by A57,REAL_LAT:def 1
.= (minreal||A). [z,"\/" (X,L)] by A13,FUNCT_1:49
.= (minreal||A).(z,"\/" (X,L))
.= z "/\" "\/" (X,L) by A11,LATTICES:def 2
.= z1 by A62,LATTICES:4;
then z1 <= y by XXREAL_0:def 9;
then y + z1 <= 1/2 + y by A60,XREAL_1:7;
then for v be Real holds not (z1 = v & 1/2 < v & v <= 1)
by XREAL_1:6;
then not z1 in { x where x is Real: 1/2 < x & x <= 1 };
hence z9 in {0} by A9,XBOOLE_0:def 3;
end;
then
A63: X c= {0};
now
per cases by A63,ZFMISC_1:33;
suppose
A64: X = {};
A65: now
let r1 be Element of L;
assume X is_less_than r1;
r1 in [.0,1.] by A13;
then r1 in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;
then consider e be Real such that
A66: r1 = e and
A67: 0 <= e and
e <= 1;
reconsider e as Real;
w "/\" r1 = (minreal||A).(w,r1) by A11,LATTICES:def 2
.= minreal. [w,r1] by A13,FUNCT_1:49
.= minreal.(w,r1)
.= min(0,e) by A66,REAL_LAT:def 1
.= w by A67,XXREAL_0:def 9;
hence w [= r1 by LATTICES:4;
end;
for q be Element of L st q in X holds q [= w by A64;
then X is_less_than w;
then "\/" (X,L) = w by A65,LATTICE3:def 21;
then "\/" (X,L) in {0} by TARSKI:def 1;
hence contradiction by A9,A59,XBOOLE_0:def 3;
end;
suppose
X = {0};
then "\/" (X,L) = w by LATTICE3:42;
then "\/" (X,L) in {0} by TARSKI:def 1;
hence contradiction by A9,A59,XBOOLE_0:def 3;
end;
end;
hence contradiction;
end;
end;
hence L9 is \/-inheriting;
now
1/2 in { x where x is Real: 0 <= x & x <= 1 };
then reconsider z = 1/2 as Element of L by A13,RCOMP_1:def 1;
set X = { x where x is Real : 1/2 < x & x <= 1 };
for y be Real holds not ( y = 1/2 & 1/2 < y & y <= 1);
then
A68: ( not 1/2 in {0})& not 1/2 in { x where x is Real: 1/2 <
x & x <= 1 } by TARSKI:def 1;
for x1 be object st x1 in { x where x is Real: 1/2 < x & x
<= 1 } holds x1 in B by A9,XBOOLE_0:def 3;
then reconsider X as Subset of L9 by TARSKI:def 3;
take X;
A69: now
let b be Element of L;
b in A by A13;
then b in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;
then consider b9 be Real such that
A70: b = b9 and
A71: 0 <= b9 and
A72: b9 <= 1;
reconsider b9 as Real;
assume
A73: b is_less_than X;
A74: b9 <= 1/2
proof
assume
A75: 1/2 < b9;
then b9 in X by A72;
then
A76: b = "/\" (X,L) by A70,A73,LATTICE3:41;
1/2 + b9 < b9 + b9 by A75,XREAL_1:6;
then
A77: (1/2 + b9)/2 < (b9 + b9)/2 by XREAL_1:74;
then (1/2 + b9)/2 + b9 <= b9 + 1 by A72,XREAL_1:7;
then
A78: (1/2 + b9)/2 <= 1 by XREAL_1:6;
then (1/2 + b9)/2 in { r : 0 <= r & r <= 1} by A71;
then reconsider c = (1/2 + b9)/2 as Element of L by A13,RCOMP_1:def 1;
reconsider cc = c as Real;
1/2 + 1/2 < b9 + 1/2 by A75,XREAL_1:6;
then 1/2 < (1/2 + b9)/2 by XREAL_1:74;
then (1/2 + b9)/2 in X by A78;
then b [= c by A76,LATTICE3:38;
then b9 = b "/\" c by A70,LATTICES:4
.= (minreal||A).(b,c) by A11,LATTICES:def 2
.= minreal. [b,c] by A13,FUNCT_1:49
.= minreal.(b,cc)
.= min(b9,(1/2 + b9)/2) by A70,REAL_LAT:def 1;
hence contradiction by A77,XXREAL_0:def 9;
end;
b "/\" z = (minreal||A).(b,z) by A11,LATTICES:def 2
.= minreal. [b,z] by A13,FUNCT_1:49
.= minreal.(b,z)
.= min(b9,jd) by A70,REAL_LAT:def 1
.= b by A70,A74,XXREAL_0:def 9;
hence b [= z by LATTICES:4;
end;
now
let q be Element of L;
assume q in X;
then
A79: ex y be Real st q = y & 1/2 < y & y <= 1;
q in A by A13;
then q in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;
then consider q9 be Real such that
A80: q = q9 and
0 <= q9 and
q9 <= 1;
reconsider q9 as Real;
z "/\" q = (minreal||A).(z,q) by A11,LATTICES:def 2
.= minreal. [z,q] by A13,FUNCT_1:49
.= minreal.(z,q)
.= min(jd,q9) by A80,REAL_LAT:def 1
.= z by A80,A79,XXREAL_0:def 9;
hence z [= q by LATTICES:4;
end;
then z is_less_than X;
then "/\"(X,L) = jd by A69,LATTICE3:34;
hence not "/\" (X,L) in the carrier of L9 by A1,A68,XBOOLE_0:def 3;
end;
hence thesis;
end;
theorem
ex L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting
non /\-inheriting
proof
reconsider L = RealSubLatt(In(0,REAL),In(1,REAL)) as complete Lattice
by Th20;
take L;
thus thesis by Th21;
end;
theorem Th23:
ex L9 be SubLattice of RealSubLatt(In(0,REAL),In(1,REAL))
st L9 is /\-inheriting
non \/-inheriting
proof
set B = {0,1} \/ ].0,1/2.[;
set L = RealSubLatt(In(0,REAL),In(1,REAL));
set R = Real_Lattice;
A1: B c= {1} \/ { x where x is Real : 0 <= x & x < 1/2 }
proof
let x1 be object;
assume
A2: x1 in B;
now
per cases by A2,XBOOLE_0:def 3;
suppose
x1 in {0,1};
then x1 = 0 or x1 = 1 by TARSKI:def 2;
then x1 in {1} or x1 in { x where x is Real : 0 <= x & x <
1/2 } by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x1 in ].0,1/2.[;
then x1 in { r : 0 < r & r < 1/2 } by RCOMP_1:def 2;
then consider y be Real such that
A3: x1 = y and
A4: 0 < y & y < 1/2;
y in { x where x is Real: 0 <= x & x < 1/2 } by A4;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
{1} \/ { x where x is Real : 0 <= x & x < 1/2 } c= B
proof
let x1 be object;
assume
A5: x1 in {1} \/ { x where x is Real : 0 <= x & x < 1/2 };
now
per cases by A5,XBOOLE_0:def 3;
suppose
x1 in {1};
then x1 = 1 by TARSKI:def 1;
then x1 in {0,1} by TARSKI:def 2;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x1 in { x where x is Real : 0 <= x & x < 1/2 };
then consider y be Real such that
A6: x1 = y and
A7: 0 <= y & y < 1/2;
y in { r : 0 < r & r < 1/2 } or y = 0 by A7;
then y in ].0,1/2.[ or y in {0,1} by RCOMP_1:def 2,TARSKI:def 2;
hence thesis by A6,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
then
A8: B = {1} \/ { x where x is Real: 0 <= x & x < 1/2 } by A1,
XBOOLE_0:def 10;
A9: 1 in { r : 0 <= r & r <= 1 };
then reconsider A = [.0,1.] as non empty set by RCOMP_1:def 1;
A10: for x1 being Element of A holds x1 is Element of R
by REAL_LAT:def 3,XREAL_0:def 1;
reconsider B as non empty set;
A11: the L_meet of L = minreal||[.0,1.] by Def4;
set Ma = maxreal||A, Mi = minreal||A;
A12: the L_join of L = maxreal||[.0,1.] by Def4;
A13: A = the carrier of L by Def4;
then reconsider Ma, Mi as BinOp of A by Def4;
A14: now
let x1 be object;
assume
A15: x1 in B;
now
per cases by A1,A15,XBOOLE_0:def 3;
suppose
x1 in {1};
then x1 = 1 by TARSKI:def 1;
hence x1 in A by A9,RCOMP_1:def 1;
end;
suppose
x1 in { x where x is Real : 0 <= x & x < 1/2 };
then consider y be Real such that
A16: x1 = y & 0 <= y and
A17: y < 1/2;
y + 1/2 <= 1/2 + 1 by A17,XREAL_1:7;
then y <= 1 by XREAL_1:6;
then x1 in { r : 0 <= r & r <= 1 } by A16;
hence x1 in A by RCOMP_1:def 1;
end;
end;
hence x1 in A;
end;
then
A18: B c= A;
then
A19: [:B,B:] c= [:A,A:] by ZFMISC_1:96;
then reconsider ma = Ma||B, mi = Mi||B as Function of [:B,B:],A by FUNCT_2:32
;
A20: dom ma = [:B,B:] by FUNCT_2:def 1;
A21: now
let x9 be object;
assume
A22: x9 in dom ma;
then consider x1,x2 be object such that
A23: x9 = [x1,x2] by RELAT_1:def 1;
A24: x2 in B by A22,A23,ZFMISC_1:87;
A25: x1 in B by A22,A23,ZFMISC_1:87;
now
per cases by A1,A25,XBOOLE_0:def 3;
suppose
x1 in {1};
then
A26: x1 = 1 by TARSKI:def 1;
now
per cases by A1,A24,XBOOLE_0:def 3;
suppose
x2 in {1};
then
A27: x2 = 1 by TARSKI:def 1;
ma.x9 = Ma. [x1,x2] by A22,A23,FUNCT_1:49
.= maxreal.(x1,x2) by A19,A22,A23,FUNCT_1:49
.= max(jj,jj) by A26,A27,REAL_LAT:def 2
.= 1;
then ma.x9 in {1} by TARSKI:def 1;
hence ma.x9 in B by A8,XBOOLE_0:def 3;
end;
suppose
x2 in { x where x is Real : 0 <= x & x < 1/2 };
then consider y2 be Real such that
A28: x2 = y2 and
A29: 0 <= y2 & y2 < 1/2;
reconsider y2 as Real;
ma.x9 = Ma. [x1,x2] by A22,A23,FUNCT_1:49
.= maxreal.(x1,x2) by A19,A22,A23,FUNCT_1:49
.= max(jj,y2) by A26,A28,REAL_LAT:def 2;
then ma.x9 = 1 or ma.x9 = y2 by XXREAL_0:16;
then ma.x9 in {1} or ma.x9 in { x where x is Real : 0
<= x & x < 1/2 } by A29,TARSKI:def 1;
hence ma.x9 in B by A8,XBOOLE_0:def 3;
end;
end;
hence ma.x9 in B;
end;
suppose
x1 in { x where x is Real : 0 <= x & x < 1/2 };
then consider y1 be Real such that
A30: x1 = y1 and
A31: 0 <= y1 & y1 < 1/2;
reconsider y1 as Real;
now
per cases by A1,A24,XBOOLE_0:def 3;
suppose
x2 in {1};
then
A32: x2 = 1 by TARSKI:def 1;
ma.x9 = Ma. [x1,x2] by A22,A23,FUNCT_1:49
.= maxreal.(x1,x2) by A19,A22,A23,FUNCT_1:49
.= max(y1,jj) by A30,A32,REAL_LAT:def 2;
then ma.x9 = y1 or ma.x9 = 1 by XXREAL_0:16;
then ma.x9 in { x where x is Real : 0 <= x & x < 1/2 }
or ma.x9 in {1} by A31,TARSKI:def 1;
hence ma.x9 in B by A8,XBOOLE_0:def 3;
end;
suppose
x2 in { x where x is Real : 0 <= x & x < 1/2 };
then consider y2 be Real such that
A33: x2 = y2 and
A34: 0 <= y2 & y2 < 1/2;
reconsider y2 as Real;
ma.x9 = Ma. [x1,x2] by A22,A23,FUNCT_1:49
.= maxreal.(x1,x2) by A19,A22,A23,FUNCT_1:49
.= max(y1,y2) by A30,A33,REAL_LAT:def 2;
then ma.x9 = y1 or ma.x9 = y2 by XXREAL_0:16;
then ma.x9 in { x where x is Real : 0 <= x & x < 1/2 }
by A31,A34;
hence ma.x9 in B by A8,XBOOLE_0:def 3;
end;
end;
hence ma.x9 in B;
end;
end;
hence ma.x9 in B;
end;
A35: dom mi = [:B,B:] by FUNCT_2:def 1;
A36: now
let x9 be object;
assume
A37: x9 in dom mi;
then consider x1,x2 be object such that
A38: x9 = [x1,x2] by RELAT_1:def 1;
A39: x2 in B by A37,A38,ZFMISC_1:87;
A40: x1 in B by A37,A38,ZFMISC_1:87;
now
per cases by A1,A40,XBOOLE_0:def 3;
suppose
x1 in {1};
then
A41: x1 = 1 by TARSKI:def 1;
now
per cases by A1,A39,XBOOLE_0:def 3;
suppose
x2 in {1};
then
A42: x2 = 1 by TARSKI:def 1;
mi.x9 = Mi. [x1,x2] by A37,A38,FUNCT_1:49
.= minreal.(x1,x2) by A19,A37,A38,FUNCT_1:49
.= min(jj,jj) by A41,A42,REAL_LAT:def 1
.= 1;
then mi.x9 in {1} by TARSKI:def 1;
hence mi.x9 in B by A8,XBOOLE_0:def 3;
end;
suppose
x2 in { x where x is Real : 0 <= x & x < 1/2 };
then consider y2 be Real such that
A43: x2 = y2 and
A44: 0 <= y2 & y2 < 1/2;
reconsider y2 as Real;
mi.x9 = Mi. [x1,x2] by A37,A38,FUNCT_1:49
.= minreal.(x1,x2) by A19,A37,A38,FUNCT_1:49
.= min(jj,y2) by A41,A43,REAL_LAT:def 1;
then mi.x9 = 1 or mi.x9 = y2 by XXREAL_0:15;
then mi.x9 in {1} or mi.x9 in { x where x is Real : 0
<= x & x < 1/2 } by A44,TARSKI:def 1;
hence mi.x9 in B by A8,XBOOLE_0:def 3;
end;
end;
hence mi.x9 in B;
end;
suppose
x1 in { x where x is Real : 0 <= x & x < 1/2 };
then consider y1 be Real such that
A45: x1 = y1 and
A46: 0 <= y1 & y1 < 1/2;
reconsider y1 as Real;
now
per cases by A1,A39,XBOOLE_0:def 3;
suppose
x2 in {1};
then
A47: x2 = 1 by TARSKI:def 1;
mi.x9 = Mi. [x1,x2] by A37,A38,FUNCT_1:49
.= minreal.(x1,x2) by A19,A37,A38,FUNCT_1:49
.= min(y1,jj) by A45,A47,REAL_LAT:def 1;
then mi.x9 = y1 or mi.x9 = 1 by XXREAL_0:15;
then mi.x9 in { x where x is Real : 0 <= x & x < 1/2 }
or mi.x9 in {1} by A46,TARSKI:def 1;
hence mi.x9 in B by A8,XBOOLE_0:def 3;
end;
suppose
x2 in { x where x is Real : 0 <= x & x < 1/2 };
then consider y2 be Real such that
A48: x2 = y2 and
A49: 0 <= y2 & y2 < 1/2;
reconsider y2 as Real;
mi.x9 = Mi. [x1,x2] by A37,A38,FUNCT_1:49
.= minreal.(x1,x2) by A19,A37,A38,FUNCT_1:49
.= min(y1,y2) by A45,A48,REAL_LAT:def 1;
then mi.x9 = y1 or mi.x9 = y2 by XXREAL_0:15;
then mi.x9 in { x where x is Real : 0 <= x & x < 1/2 }
by A46,A49;
hence mi.x9 in B by A8,XBOOLE_0:def 3;
end;
end;
hence mi.x9 in B;
end;
end;
hence mi.x9 in B;
end;
reconsider L as complete Lattice by Th20;
reconsider mi as BinOp of B by A35,A36,FUNCT_2:3;
reconsider ma as BinOp of B by A20,A21,FUNCT_2:3;
reconsider L9 = LattStr (# B, ma, mi #) as non empty LattStr;
A50: now
let a,b be Element of L9;
thus a"\/"b = (the L_join of L9).(a,b) by LATTICES:def 1
.= (maxreal||A). [a,b] by FUNCT_1:49
.= maxreal.(a,b) by A19,FUNCT_1:49;
thus a"/\"b = (the L_meet of L9).(a,b) by LATTICES:def 2
.= (minreal||A). [a,b] by FUNCT_1:49
.= minreal.(a,b) by A19,FUNCT_1:49;
end;
A51: now
let x1 be Element of B;
per cases by A8,XBOOLE_0:def 3;
suppose
x1 in {1};
then x1 = 1 by TARSKI:def 1;
hence x1 is Element of L by A9,A13,RCOMP_1:def 1;
end;
suppose
x1 in { x where x is Real: 0 <= x & x < 1/2 };
then consider y be Real such that
A52: x1 = y & 0 <= y and
A53: y < 1/2;
y + 1/2 <= 1/2 + 1 by A53,XREAL_1:7;
then y <= 1 by XREAL_1:6;
then x1 in { r : 0 <= r & r <= 1 } by A52;
hence x1 is Element of L by A13,RCOMP_1:def 1;
end;
end;
A54: now
let p,q be Element of L9;
reconsider p9 = p, q9 = q as Element of L by A51;
reconsider p9, q9 as Element of R by A13,A10;
thus p"\/"q = maxreal.(p,q) by A50
.= maxreal.(q9,p9) by REAL_LAT:1
.= q"\/"p by A50;
end;
A55: now
let p,q be Element of L9;
reconsider p9 = p, q9 = q as Element of L by A51;
reconsider p9, q9 as Element of R by A13,A10;
thus p"/\"(p"\/"q) = minreal.(p,p"\/"q) by A50
.= minreal.(p9,maxreal.(p9,q9)) by A50
.= p by REAL_LAT:6;
end;
A56: now
let p,q be Element of L9;
reconsider p9 = p, q9 = q as Element of L by A51;
reconsider p9, q9 as Element of R by A13,A10;
thus p"/\"q = minreal.(p,q) by A50
.= minreal.(q9,p9) by REAL_LAT:2
.= q"/\"p by A50;
end;
A57: now
let p,q be Element of L9;
reconsider p9 = p, q9 = q as Element of L by A51;
reconsider p9, q9 as Element of R by A13,A10;
thus (p"/\"q)"\/"q = maxreal.(p"/\"q,q) by A50
.= maxreal.(minreal.(p9,q9),q9) by A50
.= q by REAL_LAT:5;
end;
A58: now
let p,q,r be Element of L9;
reconsider p9 = p, q9 = q, r9 = r as Element of L by A51;
reconsider p9, q9, r9 as Element of R by A13,A10;
thus p"/\"(q"/\"r) = minreal.(p,q"/\"r) by A50
.= minreal.(p,minreal.(q,r)) by A50
.= minreal.(minreal.(p9,q9),r9) by REAL_LAT:4
.= minreal.(p"/\"q,r) by A50
.= (p"/\"q)"/\"r by A50;
end;
now
let p,q,r be Element of L9;
reconsider p9 = p, q9 = q, r9 = r as Element of L by A51;
reconsider p9, q9, r9 as Element of R by A13,A10;
thus p"\/"(q"\/"r) = maxreal.(p,q"\/"r) by A50
.= maxreal.(p,maxreal.(q,r)) by A50
.= maxreal.(maxreal.(p9,q9),r9) by REAL_LAT:3
.= maxreal.(p"\/"q,r) by A50
.= (p"\/"q)"\/"r by A50;
end;
then L9 is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A54,A57,A56,A58,A55,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
then reconsider L9 as Lattice;
reconsider L9 as SubLattice of RealSubLatt(In(0,REAL),In(1,REAL))
by A13,A12,A11,A18,
NAT_LAT:def 12;
take L9;
now
let X be Subset of L9;
thus "/\" (X,L) in the carrier of L9
proof
1 in { r : 0 <= r & r <= 1 };
then reconsider w = 1 as Element of L by A13,RCOMP_1:def 1;
A59: "/\" (X,L) is_less_than X by LATTICE3:34;
"/\" (X,L) in [.0,1.] by A13;
then "/\" (X,L) in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;
then consider y be Real such that
A60: y = "/\" (X,L) and
A61: 0 <= y and
y <= 1;
reconsider y as Real;
assume
A62: not "/\" (X,L) in the carrier of L9;
then not "/\" (X,L) in { x where x is Real : 0 <= x & x < 1/
2 } by A8,XBOOLE_0:def 3;
then
A63: 1/2 <= y by A60,A61;
now
let z9 be object;
assume
A64: z9 in X;
then reconsider z = z9 as Element of L9;
reconsider z as Element of L by A13,A14;
A65: "/\" (X,L) [= z by A59,A64;
reconsider z1 = z as Real;
reconsider z1 as Real;
min(z1,y) = minreal.(z1,"/\" (X,L)) by A60,REAL_LAT:def 1
.= (minreal||A). [z,"/\" (X,L)] by A13,FUNCT_1:49
.= (minreal||A).(z,"/\" (X,L))
.= z "/\" "/\" (X,L) by A11,LATTICES:def 2
.= y by A60,A65,LATTICES:4;
then y <= z1 by XXREAL_0:def 9;
then y + 1/2 <= z1 + y by A63,XREAL_1:7;
then for v be Real holds not (z1 = v & 0 <= v & v < 1/2)
by XREAL_1:6;
then not z1 in { x where x is Real : 0 <= x & x < 1/2 };
hence z9 in {1} by A8,XBOOLE_0:def 3;
end;
then
A66: X c= {1};
now
per cases by A66,ZFMISC_1:33;
suppose
A67: X = {};
A68: now
let r1 be Element of L;
assume r1 is_less_than X;
r1 in [.0,1.] by A13;
then r1 in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;
then consider e be Real such that
A69: r1 = e and
0 <= e and
A70: e <= 1;
reconsider e as Real;
r1 "/\" w = (minreal||A).(r1,w) by A11,LATTICES:def 2
.= minreal. [r1,w] by A13,FUNCT_1:49
.= minreal.(r1,w)
.= min(e,jj) by A69,REAL_LAT:def 1
.= r1 by A69,A70,XXREAL_0:def 9;
hence r1 [= w by LATTICES:4;
end;
for q be Element of L st q in X holds w [= q by A67;
then w is_less_than X;
then "/\" (X,L) = w by A68,LATTICE3:34;
then "/\" (X,L) in {1} by TARSKI:def 1;
hence contradiction by A8,A62,XBOOLE_0:def 3;
end;
suppose
X = {1};
then "/\" (X,L) = w by LATTICE3:42;
then "/\" (X,L) in {1} by TARSKI:def 1;
hence contradiction by A8,A62,XBOOLE_0:def 3;
end;
end;
hence contradiction;
end;
end;
hence L9 is /\-inheriting;
now
1/2 in { x where x is Real : 0 <= x & x <= 1 };
then reconsider z = 1/2 as Element of L by A13,RCOMP_1:def 1;
set X = { x where x is Real: 0 <= x & x < 1/2 };
for y be Real holds not ( y = 1/2 & 0 <= y & y < 1/2);
then
A71: ( not 1/2 in {1})& not 1/2 in { x where x is Real : 0 <=
x & x < 1/ 2 } by TARSKI:def 1;
for x1 be object st x1 in { x where x is Real : 0 <= x & x <
1 / 2 } holds x1 in B by A8,XBOOLE_0:def 3;
then reconsider X as Subset of L9 by TARSKI:def 3;
take X;
A72: now
let b be Element of L;
b in A by A13;
then b in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;
then consider b9 be Real such that
A73: b = b9 and
A74: 0 <= b9 and
A75: b9 <= 1;
reconsider b9 as Real;
assume
A76: X is_less_than b;
A77: 1/2 <= b9
proof
1/2 + b9 <= 1 + 1 by A75,XREAL_1:7;
then (1/2 + b9)/2 <= (1 + 1)/2 by XREAL_1:72;
then (1/2 + b9)/2 in { r : 0 <= r & r <= 1} by A74;
then reconsider c = (1/2 + b9)/2 as Element of L by A13,RCOMP_1:def 1;
reconsider cc = c as Real;
assume
A78: b9 < 1/2;
then b9 + b9 < 1/2 + b9 by XREAL_1:6;
then
A79: (b9 + b9)/2 < (1/2 + b9)/2 by XREAL_1:74;
b9 + 1/2 < 1/2 + 1/2 by A78,XREAL_1:6;
then (1/2 + b9)/2 < 1/2 by XREAL_1:74;
then
A80: (jd + b9)/2 in X by A74;
b9 in X by A74,A78;
then b = "\/" (X,L) by A73,A76,LATTICE3:40;
then c [= b by A80,LATTICE3:38;
then (1/2 + b9)/2 = c "/\" b by LATTICES:4
.= (minreal||A).(c,b) by A11,LATTICES:def 2
.= minreal. [c,b] by A13,FUNCT_1:49
.= minreal.(cc,b)
.= min((1/2 + b9)/2,b9) by A73,REAL_LAT:def 1;
hence contradiction by A79,XXREAL_0:def 9;
end;
z "/\" b = (minreal||A).(z,b) by A11,LATTICES:def 2
.= minreal. [z,b] by A13,FUNCT_1:49
.= minreal.(z,b)
.= min(jd,b9) by A73,REAL_LAT:def 1
.= z by A77,XXREAL_0:def 9;
hence z [= b by LATTICES:4;
end;
now
let q be Element of L;
assume q in X;
then
A81: ex y be Real st q = y & 0 <= y & y < 1/2;
q in A by A13;
then q in { r : 0 <= r & r <= 1 } by RCOMP_1:def 1;
then consider q9 be Real such that
A82: q = q9 and
0 <= q9 and
q9 <= 1;
reconsider q9 as Real;
q "/\" z = (minreal||A).(q,z) by A11,LATTICES:def 2
.= minreal. [q,z] by A13,FUNCT_1:49
.= minreal.(q,z)
.= min(q9,jd) by A82,REAL_LAT:def 1
.= q by A82,A81,XXREAL_0:def 9;
hence q [= z by LATTICES:4;
end;
then X is_less_than z;
then "\/" (X,L) = 1/2 by A72,LATTICE3:def 21;
hence not "\/" (X,L) in the carrier of L9 by A1,A71,XBOOLE_0:def 3;
end;
hence thesis;
end;
theorem
ex L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting
non \/-inheriting
proof
reconsider L = RealSubLatt(In(0,REAL),In(1,REAL)) as complete Lattice
by Th20;
take L;
thus thesis by Th23;
end;