:: Lattice of Substitutions
::
:: Copyright (c) 1997-2021 Association of Mizar Users

definition
let V, C be set ;
func SubstitutionSet (V,C) -> Subset of (Fin (PFuncs (V,C))) equals :: SUBSTLAT:def 1
{ 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)))
proof end;
end;

:: deftheorem defines SubstitutionSet SUBSTLAT:def 1 :
for V, C being set holds SubstitutionSet (V,C) = { 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 ) )
}
;

Lm1: for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite

proof end;

theorem Th1: :: SUBSTLAT:1
for V, C being set holds {} in SubstitutionSet (V,C)
proof end;

theorem Th2: :: SUBSTLAT:2
for V, C being set holds in SubstitutionSet (V,C)
proof end;

registration
let V, C be set ;
cluster SubstitutionSet (V,C) -> non empty ;
coherence
not SubstitutionSet (V,C) is empty
by Th2;
end;

definition
let V, C be set ;
let A, B be Element of SubstitutionSet (V,C);
:: original: \/
redefine func A \/ B -> Element of Fin (PFuncs (V,C));
coherence
A \/ B is Element of Fin (PFuncs (V,C))
proof end;
end;

registration
let V, C be set ;
cluster non empty for Element of SubstitutionSet (V,C);
existence
not for b1 being Element of SubstitutionSet (V,C) holds b1 is empty
proof end;
end;

registration
let V, C be set ;
cluster -> finite for Element of SubstitutionSet (V,C);
coherence
for b1 being Element of SubstitutionSet (V,C) holds b1 is finite
;
end;

definition
let V, C be set ;
let A be Element of Fin (PFuncs (V,C));
func mi A -> Element of SubstitutionSet (V,C) equals :: SUBSTLAT:def 2
{ 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
{ 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 ) ) )
}
is Element of SubstitutionSet (V,C)
proof end;
end;

:: deftheorem defines mi SUBSTLAT:def 2 :
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A = { 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 ) ) )
}
;

registration
let V, C be set ;
cluster -> functional for Element of SubstitutionSet (V,C);
coherence
for b1 being Element of SubstitutionSet (V,C) holds b1 is functional
proof end;
end;

definition
let V, C be set ;
let A, B be Element of Fin (PFuncs (V,C));
func A ^ B -> Element of Fin (PFuncs (V,C)) equals :: SUBSTLAT:def 3
{ (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;
coherence
{ (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } is Element of Fin (PFuncs (V,C))
proof end;
end;

:: deftheorem defines ^ SUBSTLAT:def 3 :
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;

theorem Th3: :: SUBSTLAT:3
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = B ^ A
proof end;

theorem Th4: :: SUBSTLAT:4
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) st B = holds
A ^ B = A
proof end;

theorem Th5: :: SUBSTLAT:5
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a, b being set st B in SubstitutionSet (V,C) & a in B & b in B & a c= b holds
a = b
proof end;

theorem Th6: :: SUBSTLAT:6
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being set st a in mi B holds
( a in B & ( for b being set st b in B & b c= a holds
b = a ) )
proof end;

registration
let V, C be set ;
cluster V1() Function-like finite for Element of PFuncs (V,C);
existence
ex b1 being Element of PFuncs (V,C) st b1 is finite
proof end;
end;

theorem Th7: :: SUBSTLAT:7
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for a being finite set st a in B & ( for b being finite set st b in B & b c= a holds
b = a ) holds
a in mi B
proof end;

theorem Th8: :: SUBSTLAT:8
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi A c= A by Th6;

theorem :: SUBSTLAT:9
for V, C being set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
mi A = {} by ;

theorem Th10: :: SUBSTLAT:10
for V, C being set
for B being Element of Fin (PFuncs (V,C))
for b being finite set st b in B holds
ex c being set st
( c c= b & c in mi B )
proof end;

theorem Th11: :: SUBSTLAT:11
for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi K = K
proof end;

theorem Th12: :: SUBSTLAT:12
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A \/ B) c= (mi A) \/ B
proof end;

theorem Th13: :: SUBSTLAT:13
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)
proof end;

theorem Th14: :: SUBSTLAT:14
for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
A ^ D c= B ^ D
proof end;

theorem Th15: :: SUBSTLAT:15
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 b, c being set st
( b in A & c in B & a = b \/ c )
proof end;

theorem :: SUBSTLAT:16
for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for b, c being Element of PFuncs (V,C) st b in A & c in B & b tolerates c holds
b \/ c in A ^ B ;

Lm2: 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 )

proof end;

theorem Th17: :: SUBSTLAT:17
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B
proof end;

theorem Th18: :: SUBSTLAT:18
for V, C being set
for A, B, D being Element of Fin (PFuncs (V,C)) st A c= B holds
D ^ A c= D ^ B
proof end;

theorem Th19: :: SUBSTLAT:19
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) ^ B) = mi (A ^ B)
proof end;

theorem Th20: :: SUBSTLAT:20
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ (mi B)) = mi (A ^ B)
proof end;

theorem Th21: :: SUBSTLAT:21
for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L ^ M) = (K ^ L) ^ M
proof end;

theorem Th22: :: SUBSTLAT:22
for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)
proof end;

Lm3: 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 )

proof end;

Lm4: for V, C being set
for K, L being Element of Fin (PFuncs (V,C)) holds mi ((K ^ L) \/ L) = mi L

proof end;

theorem Th23: :: SUBSTLAT:23
for V, C being set
for B being Element of Fin (PFuncs (V,C)) holds B c= B ^ B
proof end;

theorem Th24: :: SUBSTLAT:24
for V, C being set
for A being Element of Fin (PFuncs (V,C)) holds mi (A ^ A) = mi A
proof end;

theorem :: SUBSTLAT:25
for V, C being set
for K being Element of SubstitutionSet (V,C) holds mi (K ^ K) = K
proof end;

definition
let V, C be set ;
func SubstLatt (V,C) -> strict LattStr means :Def4: :: SUBSTLAT:def 4
( 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) ) ) )
proof end;
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
proof end;
end;

:: deftheorem Def4 defines SubstLatt SUBSTLAT:def 4 :
for V, C being set
for b3 being strict LattStr holds
( b3 = SubstLatt (V,C) iff ( the carrier of b3 = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds
( the L_join of b3 . (A,B) = mi (A \/ B) & the L_meet of b3 . (A,B) = mi (A ^ B) ) ) ) );

registration
let V, C be set ;
cluster SubstLatt (V,C) -> non empty strict ;
coherence
not SubstLatt (V,C) is empty
proof end;
end;

Lm5: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "\/" b = b "\/" a

proof end;

Lm6: for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof end;

Lm7: 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

proof end;

Lm8: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds (a "/\" b) "\/" b = b

proof end;

Lm9: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" b = b "/\" a

proof end;

Lm10: for V, C being set
for a, b, c being Element of (SubstLatt (V,C)) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof end;

Lm11: 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)))

proof end;

Lm12: for V, C being set
for a, b being Element of (SubstLatt (V,C)) holds a "/\" (a "\/" b) = a

proof end;

registration
let V, C be set ;
coherence
SubstLatt (V,C) is Lattice-like
proof end;
end;

registration
let V, C be set ;
coherence
( SubstLatt (V,C) is distributive & SubstLatt (V,C) is bounded )
proof end;
end;

theorem :: SUBSTLAT:26
for V, C being set holds Bottom (SubstLatt (V,C)) = {}
proof end;

theorem :: SUBSTLAT:27
for V, C being set holds Top (SubstLatt (V,C)) =
proof end;