:: by Adam Grabowski

::

:: Received May 21, 1997

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

definition

let V, C be set ;

{ 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;
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 ) ) } ;

{ 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;

:: 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 ) ) } ;

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;

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

end;
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;

registration

let V, C be set ;

existence

not for b_{1} being Element of SubstitutionSet (V,C) holds b_{1} is empty

end;
existence

not for b

proof end;

registration

let V, C be set ;

coherence

for b_{1} being Element of SubstitutionSet (V,C) holds b_{1} is finite
;

end;
coherence

for b

definition

let V, C be set ;

let A be Element of Fin (PFuncs (V,C));

{ 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)

end;
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 ) ) ) } ;

{ 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;

:: 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 ) ) ) } ;

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 ;

coherence

for b_{1} being Element of SubstitutionSet (V,C) holds b_{1} is functional

end;
coherence

for b

proof end;

definition

let V, C be set ;

let A, B be Element of Fin (PFuncs (V,C));

{ (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))

end;
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 ) } ;

{ (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;

:: 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 ) } ;

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

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

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

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 :: SUBSTLAT:9

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 )

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

for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)

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 )

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

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

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;

definition

let V, C be set ;

ex b_{1} being strict LattStr st

( the carrier of b_{1} = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds

( the L_join of b_{1} . (A,B) = mi (A \/ B) & the L_meet of b_{1} . (A,B) = mi (A ^ B) ) ) )

for b_{1}, b_{2} being strict LattStr st the carrier of b_{1} = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds

( the L_join of b_{1} . (A,B) = mi (A \/ B) & the L_meet of b_{1} . (A,B) = mi (A ^ B) ) ) & the carrier of b_{2} = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds

( the L_join of b_{2} . (A,B) = mi (A \/ B) & the L_meet of b_{2} . (A,B) = mi (A ^ B) ) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) ) );

ex b

( the carrier of b

( the L_join of b

proof end;

uniqueness for b

( the L_join of b

( the L_join of b

b

proof end;

:: deftheorem Def4 defines SubstLatt SUBSTLAT:def 4 :

for V, C being set

for b_{3} being strict LattStr holds

( b_{3} = SubstLatt (V,C) iff ( the carrier of b_{3} = SubstitutionSet (V,C) & ( for A, B being Element of SubstitutionSet (V,C) holds

( the L_join of b_{3} . (A,B) = mi (A \/ B) & the L_meet of b_{3} . (A,B) = mi (A ^ B) ) ) ) );

for V, C being set

for b

( b

( the L_join of b

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 distributive & SubstLatt (V,C) is bounded )

end;
coherence

( SubstLatt (V,C) is distributive & SubstLatt (V,C) is bounded )

proof end;