:: Lattice of Substitutions
:: by Adam Grabowski
::
:: Received May 21, 1997
:: Copyright (c) 1997-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 SUBSET_1, FINSUB_1, PARTFUN1, FINSET_1, TARSKI, XBOOLE_0,
NORMFORM, FUNCT_1, ORDINAL4, FUNCT_4, STRUCT_0, LATTICES, BINOP_1,
EQREL_1, XXREAL_2, SUBSTLAT;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, FINSUB_1, BINOP_1, STRUCT_0,
FUNCT_1, PARTFUN1, LATTICES, FUNCT_4;
constructors BINOP_1, FUNCT_4, FINSUB_1, LATTICES, RELSET_1;
registrations XBOOLE_0, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1, LATTICES,
FUNCT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICES, XBOOLE_0;
equalities LATTICES;
expansions TARSKI, XBOOLE_0;
theorems ZFMISC_1, TARSKI, FINSUB_1, FINSET_1, FUNCT_4, PARTFUN1, BINOP_1,
LATTICES, LATTICE2, XBOOLE_0, XBOOLE_1, RELSET_1;
schemes FRAENKEL, BINOP_1;
begin :: Preliminaries
reserve V, C for set;
definition
let V, C;
func SubstitutionSet (V, C) -> Subset of Fin PFuncs (V, C) equals
{ A where
A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is
finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s
c= t implies s = t ) };
coherence
proof
set IT = { A where A is Element of Fin PFuncs (V,C) : ( for u being set st
u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s
in A & t in A & s c= t implies s = t ) };
IT c= Fin PFuncs (V,C)
proof
let x be object;
assume x in IT;
then
ex B be Element of Fin PFuncs (V,C) st B = x &( for u being set st u
in B holds u is finite)& for s, t being Element of PFuncs (V, C) holds ( s in B
& t in B & s c= t implies s = t );
hence thesis;
end;
hence thesis;
end;
end;
Lm1: for a, b be set st b in SubstitutionSet (V, C) & a in b holds a is finite
proof
let a, b be set;
assume that
A1: b in SubstitutionSet (V, C) and
A2: a in b;
ex A being Element of Fin PFuncs (V,C) st A = b &( for u being set st u
in A holds u is finite)& for s, t being Element of PFuncs (V, C ) holds ( s in
A & t in A & s c= t implies s = t ) by A1;
hence thesis by A2;
end;
theorem Th1:
{} in SubstitutionSet (V, C)
proof
{} c= PFuncs (V,C);
then
A1: {} in Fin PFuncs (V,C) by FINSUB_1:def 5;
( for u being set st u in {} holds u is finite)& for s, t being Element
of PFuncs (V, C) holds ( s in {} & t in {} & s c= t implies s = t );
hence thesis by A1;
end;
theorem Th2:
{ {} } in SubstitutionSet (V, C)
proof
A1: for s, t being Element of PFuncs (V,C) holds ( s in { {} } & t in { {} }
& s c= t implies s = t )
proof
let s, t be Element of PFuncs (V,C);
assume that
A2: s in { {} } and
A3: t in { {} } and
s c= t;
s = {} by A2,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
{} is PartFunc of V,C by RELSET_1:12;
then {} in PFuncs (V,C) by PARTFUN1:45;
then { {} } c= PFuncs (V,C) by ZFMISC_1:31;
then
A4: { {} } in Fin PFuncs (V,C) by FINSUB_1:def 5;
for u being set st u in { {} } holds u is finite;
hence thesis by A4,A1;
end;
registration
let V, C;
cluster SubstitutionSet (V, C) -> non empty;
coherence by Th2;
end;
definition
let V, C;
let A, B be Element of SubstitutionSet (V, C);
redefine func A \/ B -> Element of Fin PFuncs (V, C); :: redefines \/ (XBOOLE_0, definition)
coherence
proof
A \/ B in Fin PFuncs (V, C);
hence thesis;
end;
end;
registration
let V, C;
cluster non empty for Element of SubstitutionSet (V, C);
existence
proof
{ {} } in SubstitutionSet (V, C) by Th2;
hence thesis;
end;
end;
registration
let V, C;
cluster -> finite for Element of SubstitutionSet (V, C);
coherence;
end;
definition
let V, C;
let A be Element of Fin PFuncs (V, C);
func mi A -> Element of SubstitutionSet (V, C) equals
{ t where t is Element
of PFuncs (V, C) : t is finite & for s being Element of PFuncs (V, C) holds ( s
in A & s c= t iff s = t ) };
coherence
proof
set M = { t where t is Element of PFuncs (V, C) : t is finite & for s
being Element of PFuncs (V, C) holds ( s in A & s c= t iff s = t ) };
A1: M c= PFuncs (V,C)
proof
let a be object;
assume a in M;
then
ex t9 being Element of PFuncs (V, C) st a = t9 & t9 is finite & for s
being Element of PFuncs (V, C) holds ( s in A & s c= t9 iff s = t9 );
hence thesis;
end;
A2: now
let x be object;
assume x in M;
then ex t being Element of PFuncs (V, C) st x = t & t is finite & for s
being Element of PFuncs (V, C) holds s in A & s c= t iff s = t;
hence x in A;
end;
then
A3: M c= A;
reconsider M as set;
reconsider M9 = M as Element of Fin PFuncs (V,C) by A1,A3,FINSUB_1:def 5;
A4: for u being set st u in M9 holds u is finite
proof
let u be set;
assume u in M9;
then ex t9 being Element of PFuncs (V, C) st u = t9 & t9 is finite & for
s being Element of PFuncs (V, C) holds ( s in A & s c= t9 iff s = t9 );
hence thesis;
end;
for s, t being Element of PFuncs (V, C) holds ( s in M9 & t in M9 & s
c= t implies s = t )
proof
let s, t be Element of PFuncs (V, C);
assume that
A5: s in M9 & t in M9 and
A6: s c= t;
s in A & ex tt being Element of PFuncs (V, C) st t = tt & tt is
finite & for ss being Element of PFuncs (V, C) holds ( ss in A & ss c= tt iff
ss = tt ) by A2,A5;
hence thesis by A6;
end;
then
M in { A1 where A1 is Element of Fin PFuncs (V,C) : ( for u being set
st u in A1 holds u is finite ) & for s, t being Element of PFuncs (V, C) holds
( s in A1 & t in A1 & s c= t implies s = t ) } by A4;
hence thesis;
end;
end;
registration
let V, C;
cluster -> functional for Element of SubstitutionSet(V, C);
coherence
proof
let A be Element of SubstitutionSet (V, C);
A c= PFuncs (V,C) by FINSUB_1:def 5;
hence thesis;
end;
end;
definition
let V, C;
let A, B be Element of Fin PFuncs (V, C);
func A^B -> Element of Fin PFuncs (V, C) equals
{ s \/ t where s,t is
Element of PFuncs (V,C) : s in A & t in B & s tolerates t };
coherence
proof
deffunc U(Element of PFuncs (V,C),Element of PFuncs (V,C)) = $1 \/ $2;
set M = { U(s,t) where s,t is Element of PFuncs (V,C) : s in A & t in B &
s tolerates t }, N = { U(s,t) where s,t is Element of PFuncs (V,C) : s in A & t
in B };
A1: M c= N
proof
let a be object;
assume a in M;
then
ex s,t being Element of PFuncs (V,C) st a = s \/ t & s in A & t in B
& s tolerates t;
hence thesis;
end;
A2: M c= PFuncs (V, C)
proof
let y be object;
assume y in M;
then consider s,t being Element of PFuncs (V,C) such that
A3: y = s \/ t and
s in A and
t in B and
A4: s tolerates t;
reconsider s99 = s, t99 = t as PartFunc of V,C by PARTFUN1:47;
reconsider s9 = s, t9 = t as Function;
s is PartFunc of V, C & t is PartFunc of V, C by PARTFUN1:47;
then s9 +* t9 is PartFunc of V,C by FUNCT_4:40;
then s99 \/ t99 is PartFunc of V,C by A4,FUNCT_4:30;
hence thesis by A3,PARTFUN1:45;
end;
A5: B is finite;
A6: A is finite;
N is finite from FRAENKEL:sch 22(A6,A5);
hence thesis by A1,A2,FINSUB_1:def 5;
end;
end;
reserve A, B, D for Element of Fin PFuncs (V, C);
theorem Th3:
A^B = B^A
proof
deffunc U(Element of PFuncs (V,C),Element of PFuncs (V,C)) = $1 \/ $2;
defpred X[Function,Function] means $1 in A & $2 in B & $1 tolerates $2;
defpred Y[Function,Function] means $2 in B & $1 in A & $2 tolerates $1;
set X1 = { U(s,t) where s is Element of PFuncs (V,C), t is Element of PFuncs
(V,C) : X[s,t] };
set X2 = { U(t,s) where s is Element of PFuncs (V,C), t is Element of PFuncs
(V,C) : Y[s,t] };
A1: now
let x be object;
x in X2 iff ex s,t being Element of PFuncs (V,C) st x = U(t,s) & Y[s,t ];
then
x in X2 iff ex t,s being Element of PFuncs (V,C) st x = t \/ s & t in
B & s in A & t tolerates s;
hence x in X2 iff x in { t \/ s where t is Element of PFuncs (V,C), s is
Element of PFuncs (V,C) : t in B & s in A & t tolerates s };
end;
A2: for s, t being Element of PFuncs (V,C) holds U(s,t) = U(t,s);
A3: for s, t being Element of PFuncs (V,C) holds X[s,t] iff Y[s,t];
X1 = X2 from FRAENKEL:sch 8(A3,A2);
hence thesis by A1,TARSKI:2;
end;
theorem Th4:
B = { {} } implies A ^ B = A
proof
A1: { s \/ t where s,t is Element of PFuncs (V,C) : s in A & t in { {} } & s
tolerates t } c= A
proof
let a be object;
assume a in { s \/ t where s,t is Element of PFuncs (V,C) : s in A & t in
{ {} } & s tolerates t };
then consider s9, t9 being Element of PFuncs (V,C) such that
A2: a = s9 \/ t9 & s9 in A and
A3: t9 in { {} } and
s9 tolerates t9;
t9 = {} by A3,TARSKI:def 1;
hence thesis by A2;
end;
A4: A c= { s \/ t where s,t is Element of PFuncs (V,C) : s in A & t in { {}
} & s tolerates t }
proof
{} is PartFunc of V, C by RELSET_1:12;
then reconsider b = {} as Element of PFuncs (V,C) by PARTFUN1:45;
let a be object;
assume
A5: a in A;
A c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider a9 = a as Element of PFuncs (V,C) by A5;
A6: b in { {} } by TARSKI:def 1;
a = a9 \/ b & a9 tolerates b by PARTFUN1:59;
hence thesis by A5,A6;
end;
assume B = { {} };
hence thesis by A1,A4;
end;
theorem Th5:
for a, b be set holds B in SubstitutionSet (V, C) & a in B & b in
B & a c= b implies a = b
proof
let a, b be set;
assume B in SubstitutionSet (V, C);
then
A1: ex A1 be Element of Fin PFuncs (V,C) st A1 = B & ( for u being set st u
in A1 holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s
in A1 & t in A1 & s c= t implies s = t );
assume that
A2: a in B & b in B and
A3: a c= b;
B c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider a9 = a, b9 = b as Element of PFuncs (V, C) by A2;
a9 = b9 by A1,A2,A3;
hence thesis;
end;
theorem Th6:
for a be set holds a in mi B implies a in B & for b be set holds
b in B & b c= a implies b = a
proof
let a be set;
assume a in mi B;
then
A1: ex t being Element of PFuncs (V, C) st a = t & t is finite & for s being
Element of PFuncs (V, C) holds s in B & s c= t iff s = t;
hence a in B;
let b be set;
assume that
A2: b in B and
A3: b c= a;
B c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs (V, C) by A2;
b9 = a by A1,A2,A3;
hence thesis;
end;
reserve s for Element of PFuncs (V,C);
registration
let V, C;
cluster finite for Element of PFuncs (V,C);
existence
proof
{} is PartFunc of V,C by RELSET_1:12;
then reconsider e = {} as Element of PFuncs (V,C) by PARTFUN1:45;
take e;
thus thesis;
end;
end;
theorem Th7:
for a be finite set holds a in B & (for b be finite set st b in B
& b c= a holds b = a) implies a in mi B
proof
let a be finite set;
assume that
A1: a in B and
A2: for s be finite set st s in B & s c= a holds s = a;
B c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider a9 = a as Element of PFuncs (V, C) by A1;
s in B & s c= a iff s = a by A1,A2;
then
a9 in { t where t is Element of PFuncs (V,C) : t is finite & for s being
Element of PFuncs (V, C) holds s in B & s c= t iff s = t };
hence thesis;
end;
theorem Th8:
mi A c= A
by Th6;
theorem
A = {} implies mi A = {} by Th8,XBOOLE_1:3;
theorem Th10:
for b be finite set holds b in B implies ex c be set st c c= b & c in mi B
proof
defpred X[set,set] means $1 c= $2;
let b be finite set;
assume
A1: b in B;
A2: B c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider b9 = b as Element of PFuncs (V, C) by A1;
A3: for a,b,c be Element of PFuncs (V, C) st X[a,b] & X[b,c] holds X[a,c] by
XBOOLE_1:1;
A4: for a be Element of PFuncs (V, C) holds X[a,a];
for a be Element of PFuncs (V, C) st a in B ex b be Element of PFuncs (V
, C) st b in B & X[b,a] & for c be Element of PFuncs (V, C) st c in B & X[c,b]
holds X[b,c] from FRAENKEL:sch 23(A4,A3);
then consider c be Element of PFuncs (V, C) such that
A5: c in B and
A6: c c= b9 and
A7: for a be Element of PFuncs (V, C) st a in B & a c= c holds c c= a by A1;
take c;
thus c c= b by A6;
for b be finite set st b in B & b c= c holds b = c by A2,A7;
hence thesis by A5,A6,Th7;
end;
theorem Th11:
for K be Element of SubstitutionSet (V, C) holds mi K = K
proof
let K be Element of SubstitutionSet (V, C);
thus mi K c= K by Th8;
now
let a be set;
assume
A1: a in K;
then a is finite & for b be finite set st b in K & b c= a holds b = a by
Lm1,Th5;
hence a in mi K by A1,Th7;
end;
hence thesis;
end;
theorem Th12:
mi (A \/ B) c= mi A \/ B
proof
now
let a be set;
assume
A1: a in mi (A \/ B);
then reconsider a9 = a as finite set by Lm1;
A2: a in A \/ B by A1,Th6;
now
per cases by A2,XBOOLE_0:def 3;
suppose
A3: a in A;
now
let b be finite set;
assume b in A;
then b in A \/ B by XBOOLE_0:def 3;
hence b c= a implies b = a by A1,Th6;
end;
then a9 in mi A by A3,Th7;
hence a in mi A \/ B by XBOOLE_0:def 3;
end;
suppose
a in B;
hence a in mi A \/ B by XBOOLE_0:def 3;
end;
end;
hence a in mi A \/ B;
end;
hence thesis;
end;
theorem Th13:
mi(mi A \/ B) = mi (A \/ B)
proof
A1: mi A \/ B c= A \/ B by Th8,XBOOLE_1:9;
now
let a be set;
assume
A2: a in mi(mi A \/ B);
then reconsider a9 = a as finite set by Lm1;
A3: now
let b be finite set;
assume that
A4: b in A \/ B and
A5: b c= a;
now
per cases by A4,XBOOLE_0:def 3;
suppose
b in A;
then consider c be set such that
A6: c c= b and
A7: c in mi A by Th10;
c in mi A \/ B & c c= a by A5,A6,A7,XBOOLE_0:def 3;
then c = a by A2,Th6;
hence b = a by A5,A6;
end;
suppose
b in B;
then b in mi A \/ B by XBOOLE_0:def 3;
hence b = a by A2,A5,Th6;
end;
end;
hence b = a;
end;
a in mi A \/ B by A2,Th6;
then a9 in mi (A \/ B) by A1,A3,Th7;
hence a in mi (A \/ B);
end;
hence mi(mi A \/ B) c= mi (A \/ B);
A8: mi(A \/ B) c= mi A \/ B by Th12;
now
let a be set;
assume
A9: a in mi (A \/ B);
then reconsider a9 = a as finite set by Lm1;
for b be finite set st b in mi A \/ B holds b c= a implies b = a by A1,A9
,Th6;
then a9 in mi(mi A \/ B) by A8,A9,Th7;
hence a in mi(mi A \/ B);
end;
hence thesis;
end;
theorem Th14:
A c= B implies A ^ D c= B ^ D
proof
deffunc U(Element of PFuncs (V,C),Element of PFuncs (V,C)) = $1 \/ $2;
defpred X[Function,Function] means $1 in A & $2 in D & $1 tolerates $2;
defpred Y[Function,Function] means $1 in B & $2 in D & $1 tolerates $2;
set X1 = { U(s,t) where s, t is Element of PFuncs (V,C) : X[s,t]}, X2 = { U(
s,t) where s, t is Element of PFuncs (V,C) : Y[s,t]};
assume A c= B;
then
A1: for s, t being Element of PFuncs (V,C) holds X[s,t] implies Y[s,t];
X1 c= X2 from FRAENKEL:sch 2(A1);
hence thesis;
end;
theorem Th15:
for a be set holds a in A^B implies ex b,c be set st b in A & c
in B & a = b \/ c
proof
let a be set;
assume a in A^B;
then ex s,t be Element of PFuncs (V,C) st a = s \/ t & s in A & t in B & s
tolerates t;
hence thesis;
end;
theorem
for b, c be Element of PFuncs (V, C) holds b in A & c in B & b
tolerates c implies b \/ c in A^B;
Lm2: for a be finite set holds a in A ^ B implies ex b be finite set st b c= a
& b in mi A ^ B
proof
let a be finite set;
assume a in A ^ B;
then consider b, c be Element of PFuncs (V,C) such that
A1: a = b \/ c and
A2: b in A and
A3: c in B and
A4: b tolerates c;
b is finite by A1,FINSET_1:1,XBOOLE_1:7;
then consider d be set such that
A5: d c= b and
A6: d in mi A by A2,Th10;
A7: mi A c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider d9 = d, c9 = c as Element of PFuncs (V, C) by A6;
reconsider d1 = d, b1 = b, c1 = c as PartFunc of V, C by A6,A7,PARTFUN1:46;
d1 c= b1 by A5;
then
A8: d9 tolerates c9 by A4,PARTFUN1:58;
then d9 \/ c9 = d9 +* c9 by FUNCT_4:30;
then reconsider e = d1 \/ c1 as Element of PFuncs (V, C) by PARTFUN1:45;
reconsider e as finite set by A1,A5,FINSET_1:1,XBOOLE_1:9;
take e;
thus e c= a by A1,A5,XBOOLE_1:9;
thus thesis by A3,A6,A8;
end;
theorem Th17:
mi(A ^ B) c= mi A ^ B
proof
A1: mi A ^ B c= A ^ B by Th8,Th14;
now
let a be set;
assume
A2: a in mi (A ^ B);
then a in A ^ B & a is finite by Lm1,Th6;
then ex b be finite set st b c= a & b in mi A ^ B by Lm2;
hence a in mi A ^ B by A1,A2,Th6;
end;
hence thesis;
end;
theorem Th18:
A c= B implies D ^ A c= D ^ B
proof
D ^ A = A ^ D & D ^ B = B ^ D by Th3;
hence thesis by Th14;
end;
theorem Th19:
mi(mi A ^ B) = mi (A ^ B)
proof
A1: mi A ^ B c= A ^ B by Th8,Th14;
now
let a be set;
assume
A2: a in mi (mi A ^ B);
A3: now
let b be finite set;
assume b in A ^ B;
then consider c be finite set such that
A4: c c= b and
A5: c in mi A ^ B by Lm2;
assume
A6: b c= a;
then c c= a by A4;
then c = a by A2,A5,Th6;
hence b = a by A4,A6;
end;
a in mi A ^ B & a is finite by A2,Lm1,Th6;
hence a in mi (A ^ B) by A1,A3,Th7;
end;
hence mi(mi A ^ B) c= mi(A ^ B);
A7: mi(A ^ B) c= mi A ^ B by Th17;
now
let a be set;
assume
A8: a in mi(A ^ B);
then a is finite & for b be finite set st b in mi A ^ B holds b c= a
implies b = a by A1,Lm1,Th6;
hence a in mi(mi A ^ B) by A7,A8,Th7;
end;
hence thesis;
end;
theorem Th20:
mi(A ^ mi B) = mi (A ^ B)
proof
A ^ mi B = mi B ^ A & A ^ B = B ^ A by Th3;
hence thesis by Th19;
end;
theorem Th21:
for K, L, M being Element of Fin PFuncs (V, C) holds K^(L^M) = K ^L^M
proof
let K, L, M be Element of Fin PFuncs (V, C);
A1: L^M = M^L & K^L = L^K by Th3;
A2: now
let K, L, M be Element of Fin PFuncs (V, C);
A3: K c= PFuncs (V,C) & L c= PFuncs (V,C) by FINSUB_1:def 5;
A4: M c= PFuncs (V,C) by FINSUB_1:def 5;
now
let a be set;
A5: K^(L^M) c= PFuncs (V,C) by FINSUB_1:def 5;
assume
A6: a in K^(L^M);
then consider b,c be set such that
A7: b in K and
A8: c in L^M and
A9: a = b \/ c by Th15;
A10: c c= b \/ c by XBOOLE_1:7;
consider b1, c1 being set such that
A11: b1 in L and
A12: c1 in M and
A13: c = b1 \/ c1 by A8,Th15;
reconsider b2 = b, b12 = b1 as PartFunc of V, C by A3,A7,A11,PARTFUN1:46;
reconsider b9 = b, b19 = b1, c19 = c1 as Element of PFuncs (V,C) by A3,A4
,A7,A11,A12;
b1 c= c by A13,XBOOLE_1:7;
then
A14: b c= b \/ c & b1 c= b \/ c by A10,XBOOLE_1:7;
then
A15: b9 tolerates b19 by A6,A9,A5,PARTFUN1:57;
then b9 \/ b19 = b9 +* b19 by FUNCT_4:30;
then b2 \/ b12 is PartFunc of V, C;
then reconsider c2 = b9 \/ b19 as Element of PFuncs (V,C) by PARTFUN1:45;
A16: b \/ (b1 \/ c1) = b \/ b1 \/ c1 & c2 in K^L by A7,A11,A15,XBOOLE_1:4;
c1 c= c by A13,XBOOLE_1:7;
then
A17: c1 c= b \/ c by A10;
c2 c= b \/ c by A14,XBOOLE_1:8;
then c2 tolerates c19 by A6,A9,A5,A17,PARTFUN1:57;
hence a in K^L^M by A9,A12,A13,A16;
end;
hence K^(L^M) c= K^L^M;
end;
then
A18: K^(L^M) c= K^L^M;
K^L^M = M^(K^L) & K^(L^M) = L^M^K by Th3;
then K^L^M c= K^(L^M) by A1,A2;
hence thesis by A18;
end;
theorem Th22:
for K, L, M being Element of Fin PFuncs (V, C) holds K^(L \/ M) = K^L \/ K^M
proof
let K, L, M be Element of Fin PFuncs (V, C);
now
let a be set;
assume
A1: a in K^(L \/ M);
then consider b,c being set such that
A2: b in K and
A3: c in L \/ M and
A4: a = b \/ c by Th15;
K^(L \/ M) c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
K c= PFuncs (V, C) & L \/ M c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider b9 = b, c9 = c as Element of PFuncs (V,C) by A2,A3;
b9 c= a9 & c9 c= a9 by A4,XBOOLE_1:7;
then
A5: b9 tolerates c9 by PARTFUN1:57;
c9 in L or c9 in M by A3,XBOOLE_0:def 3;
then a in K^L or a in K^M by A2,A4,A5;
hence a in K^L \/ K^M by XBOOLE_0:def 3;
end;
hence K^(L \/ M) c= K^L \/ K^M;
K^L c= K^(L \/ M) & K^M c= K^(L \/ M) by Th18,XBOOLE_1:7;
hence thesis by XBOOLE_1:8;
end;
Lm3: for a be set holds a in A ^ B implies ex c be set st c in B & c c= a
proof
let a be set;
assume a in A ^ B;
then consider b,c be set such that
b in A and
A1: c in B and
A2: a = b \/ c by Th15;
take c;
thus c in B by A1;
thus thesis by A2,XBOOLE_1:7;
end;
Lm4: for K, L being Element of Fin PFuncs (V, C) holds mi(K ^ L \/ L) = mi L
proof
let K, L be Element of Fin PFuncs (V, C);
now
let a be set;
assume
A1: a in mi(K ^ L \/ L);
then a in K ^ L \/ L by Th6;
then
A2: a in K ^ L or a in L by XBOOLE_0:def 3;
A3: now
let b be finite set;
assume b in L;
then b in K ^ L \/ L by XBOOLE_0:def 3;
hence b c= a implies b = a by A1,Th6;
end;
A4: now
assume a in K ^ L;
then consider b be set such that
A5: b in L and
A6: b c= a by Lm3;
b in K ^ L \/ L by A5,XBOOLE_0:def 3;
hence a in L by A1,A5,A6,Th6;
end;
a is finite by A1,Lm1;
hence a in mi L by A2,A4,A3,Th7;
end;
hence mi(K ^ L \/ L) c= mi L;
now
let a be set;
assume
A7: a in mi L;
then
A8: a in L by Th6;
then
A9: a in K ^ L \/ L by XBOOLE_0:def 3;
A10: now
let b be finite set;
assume b in K ^ L \/ L;
then
A11: b in K ^ L or b in L by XBOOLE_0:def 3;
assume
A12: b c= a;
now
assume b in K ^ L;
then consider c be set such that
A13: c in L and
A14: c c= b by Lm3;
c c= a by A12,A14;
then c = a by A7,A13,Th6;
hence b in L by A8,A12,A14,XBOOLE_0:def 10;
end;
hence b = a by A7,A11,A12,Th6;
end;
a is finite by A7,Lm1;
hence a in mi(K ^ L \/ L) by A9,A10,Th7;
end;
hence thesis;
end;
theorem Th23:
B c= B ^ B
proof
now
let a be set;
assume
A1: a in B;
B c= PFuncs (V, C) by FINSUB_1:def 5;
then reconsider a9 = a as Element of PFuncs (V,C) by A1;
a = a \/ a & a9 tolerates a9;
hence a in B ^ B by A1;
end;
hence thesis;
end;
theorem Th24:
mi (A ^ A) = mi A
proof
thus mi (A ^ A) = mi (A ^ A \/ A) by Th23,XBOOLE_1:12
.= mi A by Lm4;
end;
theorem
for K be Element of SubstitutionSet (V, C) holds mi (K^K) = K
proof
let K be Element of SubstitutionSet (V, C);
thus mi (K^K) = mi K by Th24
.= K by Th11;
end;
begin :: Definition of the lattice
definition
let V, C;
func SubstLatt (V, C) -> strict LattStr means
:Def4:
the carrier of it =
SubstitutionSet (V, C) & for A, B being Element of SubstitutionSet (V, C) holds
(the L_join of it).(A,B) = mi (A \/ B) & (the L_meet of it).(A,B) = mi (A^B);
existence
proof
deffunc U(Element of SubstitutionSet (V, C), Element of SubstitutionSet (V
, C)) = mi ($1 \/ $2);
consider j being BinOp of SubstitutionSet (V, C) such that
A1: for x,y being Element of SubstitutionSet (V, C) holds j.(x,y) = U(
x,y) from BINOP_1:sch 4;
deffunc U(Element of SubstitutionSet (V, C), Element of SubstitutionSet (V
, C)) = mi ($1 ^ $2);
consider m being BinOp of SubstitutionSet (V, C) such that
A2: for x,y being Element of SubstitutionSet (V, C) holds m.(x,y) = U(
x,y) from BINOP_1:sch 4;
take LattStr (# SubstitutionSet (V, C), j, m #);
thus thesis by A1,A2;
end;
uniqueness
proof
let A1, A2 be strict LattStr such that
A3: the carrier of A1 = SubstitutionSet (V, C) and
A4: for A, B being Element of SubstitutionSet (V, C) holds (the L_join
of A1).(A,B) = mi (A \/ B) & (the L_meet of A1).(A,B) = mi (A^B) and
A5: the carrier of A2 = SubstitutionSet (V, C) and
A6: for A, B being Element of SubstitutionSet (V, C) holds (the L_join
of A2).(A,B) = mi (A \/ B) & (the L_meet of A2).(A,B) = mi (A^B);
reconsider a3 = the L_meet of A1, a4 = the L_meet of A2, a1 = the L_join
of A1, a2 = the L_join of A2 as BinOp of SubstitutionSet (V, C) by A3,A5;
now
let x,y be Element of SubstitutionSet (V, C);
thus a1.(x,y) = mi (x \/ y) by A4
.= a2.(x,y) by A6;
end;
then
A7: a1 = a2 by BINOP_1:2;
now
let x,y be Element of SubstitutionSet (V, C);
thus a3.(x,y) = mi (x^y) by A4
.= a4.(x,y) by A6;
end;
hence thesis by A3,A5,A7,BINOP_1:2;
end;
end;
registration
let V, C;
cluster SubstLatt (V, C) -> non empty;
coherence
proof
the carrier of SubstLatt (V, C) = SubstitutionSet (V, C) by Def4;
hence thesis;
end;
end;
Lm5: for a,b being Element of SubstLatt (V, C) holds a"\/"b = b"\/"a
proof
set G = SubstLatt (V, C);
let a,b be Element of G;
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by Def4;
a"\/"b = mi (b9 \/ a9) by Def4
.= b"\/"a by Def4;
hence thesis;
end;
Lm6: for a,b,c being Element of SubstLatt (V, C) holds a"\/"(b"\/"c) = (a"\/"b
)"\/"c
proof
let a, b, c be Element of SubstLatt (V, C);
reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V, C) by
Def4;
set G = SubstLatt (V, C);
a"\/"(b"\/"c) = (the L_join of G).(a, mi (b9 \/ c9)) by Def4
.= mi (mi (b9 \/ c9) \/ a9) by Def4
.= mi ( a9 \/ ( b9 \/ c9 ) ) by Th13
.= mi ( a9 \/ b9 \/ c9 ) by XBOOLE_1:4
.= mi ( mi ( a9 \/ b9 ) \/ c9 ) by Th13
.= (the L_join of G).(mi (a9 \/ b9), c9 ) by Def4
.= (a"\/"b)"\/"c by Def4;
hence thesis;
end;
reserve K, L, M for Element of SubstitutionSet (V,C);
Lm7: (the L_join of SubstLatt (V, C)). ((the L_meet of SubstLatt (V, C)).(K,L)
, L) = L
proof
thus (the L_join of SubstLatt (V, C)). ((the L_meet of SubstLatt (V, C)).(K,
L), L) = (the L_join of SubstLatt (V, C)).(mi (K^L), L) by Def4
.= mi(mi(K ^ L) \/ L) by Def4
.= mi(K ^ L \/ L) by Th13
.= mi L by Lm4
.= L by Th11;
end;
Lm8: for a,b being Element of SubstLatt (V, C) holds (a"/\"b)"\/"b = b
proof
let a,b be Element of SubstLatt (V, C);
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by Def4;
set G = SubstLatt (V, C);
thus (a"/\"b)"\/"b = (the L_join of G).((the L_meet of G).(a9,b9), b9)
.= b by Lm7;
end;
Lm9: for a,b being Element of SubstLatt (V, C) holds a"/\"b = b"/\"a
proof
let a, b be Element of SubstLatt (V, C);
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by Def4;
a"/\"b = mi (a9 ^ b9) by Def4
.= mi (b9 ^ a9) by Th3
.= b"/\"a by Def4;
hence thesis;
end;
Lm10: for a,b,c being Element of SubstLatt (V, C) holds a"/\"(b"/\"c) = (a"/\"
b)"/\"c
proof
let a, b, c be Element of SubstLatt (V, C);
reconsider a9 = a, b9 = b, c9 = c as Element of SubstitutionSet (V, C) by
Def4;
set G = SubstLatt (V, C);
a"/\"(b"/\"c) = (the L_meet of G).(a, mi (b9 ^ c9)) by Def4
.= mi (a9 ^ mi (b9 ^ c9)) by Def4
.= mi ( a9 ^ ( b9 ^ c9 ) ) by Th20
.= mi ( a9 ^ b9 ^ c9 ) by Th21
.= mi ( mi ( a9 ^ b9 ) ^ c9 ) by Th19
.= (the L_meet of G).(mi (a9 ^ b9), c9 ) by Def4
.= (a"/\"b)"/\"c by Def4;
hence thesis;
end;
Lm11: (the L_meet of SubstLatt (V, C)).(K,(the L_join of SubstLatt (V, C)). (L
,M)) = (the L_join of SubstLatt (V, C)).((the L_meet of SubstLatt (V, C)).(K,L)
, (the L_meet of SubstLatt (V, C)).(K,M))
proof
A1: (the L_meet of SubstLatt (V, C)).(K,M) = mi (K ^ M) by Def4;
(the L_join of SubstLatt (V, C)).(L, M) = mi (L \/ M) & (the L_meet of
SubstLatt (V, C)).(K,L) = mi (K ^ L) by Def4;
then reconsider
La = (the L_join of SubstLatt (V, C)).(L, M), Lb = (the L_meet of
SubstLatt (V, C)).(K,L), Lc = (the L_meet of SubstLatt (V, C)).(K,M) as Element
of SubstitutionSet (V,C) by A1;
(the L_meet of SubstLatt (V, C)). (K,(the L_join of SubstLatt (V, C)).(L
,M)) = mi (K^La) by Def4
.= mi (K^mi(L \/ M)) by Def4
.= mi (K^(L \/ M)) by Th20
.= mi (K^L \/ K^M) by Th22
.= mi (mi(K^L) \/ K^M) by Th13
.= mi (mi(K^L) \/ mi (K^M)) by Th13
.= mi (Lb \/ mi(K^M)) by Def4
.= mi (Lb \/ Lc) by Def4;
hence thesis by Def4;
end;
Lm12: for a,b being Element of SubstLatt (V, C) holds a"/\"(a"\/"b)=a
proof
let a,b be Element of SubstLatt (V, C);
reconsider a9 = a, b9 = b as Element of SubstitutionSet (V, C) by Def4;
thus a"/\"(a"\/"b) = (the L_join of SubstLatt (V, C)).((the L_meet of
SubstLatt (V, C)).(a9,a9), (the L_meet of SubstLatt (V, C)).(a9,b9)) by Lm11
.= (the L_join of SubstLatt (V, C)).(mi (a9 ^ a9), (the L_meet of
SubstLatt (V, C)).(a9,b9)) by Def4
.= (the L_join of SubstLatt (V, C)).(mi a9, (the L_meet of SubstLatt (V,
C)).(a9,b9)) by Th24
.= a"\/"(a"/\"b) by Th11
.= (a"/\"b)"\/"a by Lm5
.= (b"/\"a)"\/"a by Lm9
.= a by Lm8;
end;
registration
let V, C;
cluster SubstLatt (V, C) -> Lattice-like;
coherence
proof
set G = SubstLatt (V, C);
thus for u,v being Element of G holds u"\/"v = v"\/"u by Lm5;
thus for u,v,w being Element of G holds u"\/"(v"\/"w) = (u"\/"v)"\/"w by
Lm6;
thus for u,v being Element of G holds (u"/\"v)"\/" v = v by Lm8;
thus for u,v being Element of G holds u"/\"v = v"/\" u by Lm9;
thus for u,v,w being Element of G holds u"/\"(v"/\"w) = (u"/\"v)"/\"w by
Lm10;
let u,v be Element of G;
thus thesis by Lm12;
end;
end;
registration
let V, C;
cluster SubstLatt (V, C) -> distributive bounded;
coherence
proof
thus SubstLatt (V, C) is distributive
proof
let u,v,w be Element of SubstLatt (V, C);
reconsider K = u, L = v, M = w as Element of SubstitutionSet (V,C) by
Def4;
thus u "/\" (v "\/" w) = (the L_meet of SubstLatt (V, C)).(K,(the L_join
of SubstLatt (V, C)). (L,M))
.= (u "/\" v) "\/" (u "/\" w) by Lm11;
end;
A1: SubstLatt (V, C) is lower-bounded
proof
reconsider E = {} as Element of SubstitutionSet (V,C) by Th1;
set L = SubstLatt (V, C);
reconsider e = E as Element of L by Def4;
take e;
let u be Element of L;
reconsider K = u as Element of SubstitutionSet (V,C) by Def4;
A2: e "\/" u = mi (E \/ K) by Def4
.= u by Th11;
then u "/\" e = e by LATTICES:def 9;
hence thesis by A2,LATTICES:def 9;
end;
SubstLatt (V, C) is upper-bounded
proof
reconsider E = { {} } as Element of SubstitutionSet (V,C) by Th2;
set L = SubstLatt (V, C);
reconsider e = E as Element of L by Def4;
take e;
let u be Element of L;
reconsider K = u as Element of SubstitutionSet (V,C) by Def4;
A3: e "/\" u = mi (E ^ K) by Def4
.= mi (K ^ E) by Th3
.= mi K by Th4
.= u by Th11;
then e "\/" u = e by LATTICES:def 8;
hence thesis by A3,LATTICES:def 8;
end;
hence SubstLatt (V, C) is bounded by A1;
end;
end;
theorem
Bottom SubstLatt (V,C) = {}
proof
{} in SubstitutionSet (V,C) by Th1;
then reconsider Z = {} as Element of SubstLatt (V,C) by Def4;
now
let u be Element of SubstLatt (V,C);
reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4;
thus Z "\/" u = mi (z \/ u9) by Def4
.= u by Th11;
end;
hence thesis by LATTICE2:14;
end;
theorem
Top SubstLatt (V,C) = { {} }
proof
{ {} } in SubstitutionSet (V,C) by Th2;
then reconsider Z = { {} } as Element of SubstLatt (V,C) by Def4;
now
let u be Element of SubstLatt (V,C);
reconsider z = Z, u9 = u as Element of SubstitutionSet (V,C) by Def4;
thus Z "/\" u = mi (z ^ u9) by Def4
.= mi (u9 ^ z) by Th3
.= mi u9 by Th4
.= u by Th11;
end;
hence thesis by LATTICE2:16;
end;