begin
definition
let V,
C be
set ;
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 st s in A & t in A & s c= t holds
s = t ) ) } ;
coherence
{ 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 st s in A & t in A & s c= t holds
s = t ) ) } is Subset of (Fin (PFuncs V,C))
end;
:: deftheorem defines SubstitutionSet SUBSTLAT:def 1 :
Lm1:
for V, C, a, b being set st b in SubstitutionSet V,C & a in b holds
a is finite
theorem Th1:
theorem Th2:
:: deftheorem defines mi SUBSTLAT:def 2 :
:: deftheorem defines ^ SUBSTLAT:def 3 :
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
Lm2:
for V, C being set
for A, B being Element of Fin (PFuncs V,C) st ( for a being set st a in A holds
a in B ) holds
A c= B
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
Lm3:
for V, C being set
for A, B being Element of Fin (PFuncs V,C)
for a being finite set st a in A ^ B holds
ex b being finite set st
( b c= a & b in (mi A) ^ B )
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
Lm4:
for V, C being set
for A, B being Element of Fin (PFuncs V,C)
for a being set st a in A ^ B holds
ex c being set st
( c in B & c c= a )
Lm5:
for V, C being set
for K, L being Element of Fin (PFuncs V,C) holds mi ((K ^ L) \/ L) = mi L
theorem Th23:
theorem Th24:
theorem
begin
definition
let V,
C be
set ;
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
ex b1 being strict LattStr st
( the carrier of b1 = SubstitutionSet V,C & ( for A, B being Element of SubstitutionSet V,C holds
( the L_join of b1 . A,B = mi (A \/ B) & the L_meet of b1 . A,B = mi (A ^ B) ) ) )
uniqueness
for b1, b2 being strict LattStr st the carrier of b1 = SubstitutionSet V,C & ( for A, B being Element of SubstitutionSet V,C holds
( the L_join of b1 . A,B = mi (A \/ B) & the L_meet of b1 . A,B = mi (A ^ B) ) ) & the carrier of b2 = SubstitutionSet V,C & ( for A, B being Element of SubstitutionSet V,C holds
( the L_join of b2 . A,B = mi (A \/ B) & the L_meet of b2 . A,B = mi (A ^ B) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines SubstLatt SUBSTLAT:def 4 :
Lm6:
for V, C being set
for a, b being Element of (SubstLatt V,C) holds a "\/" b = b "\/" a
Lm7:
for V, C being set
for a, b, c being Element of (SubstLatt V,C) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
Lm8:
for V, C being set
for K, L being Element of SubstitutionSet V,C holds the L_join of (SubstLatt V,C) . (the L_meet of (SubstLatt V,C) . K,L),L = L
Lm9:
for V, C being set
for a, b being Element of (SubstLatt V,C) holds (a "/\" b) "\/" b = b
Lm10:
for V, C being set
for a, b being Element of (SubstLatt V,C) holds a "/\" b = b "/\" a
Lm11:
for V, C being set
for a, b, c being Element of (SubstLatt V,C) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
Lm12:
for V, C being set
for K, L, M being Element of SubstitutionSet V,C holds 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)
Lm13:
for V, C being set
for a, b being Element of (SubstLatt V,C) holds a "/\" (a "\/" b) = a
theorem
theorem