environ
vocabularies HIDDEN, NUMBERS, PBOOLE, RELAT_1, EQREL_1, TARSKI, XBOOLE_0, STRUCT_0, LATTICES, FUNCT_1, SUBSET_1, BINOP_1, MSUALG_4, ZFMISC_1, CARD_3, MSUALG_1, FINSEQ_1, MARGREL1, PARTFUN1, ARYTM_3, ORDINAL4, NAT_1, XXREAL_0, CARD_1, RELAT_2, ARYTM_1, NAT_LAT, REALSET1, XXREAL_2, MSUALG_5, SETLIM_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, REALSET1, ORDINAL1, NUMBERS, XCMPLX_0, FINSEQ_2, STRUCT_0, PARTFUN1, FUNCT_2, RELSET_1, EQREL_1, BINOP_1, PBOOLE, MSUALG_1, MSUALG_3, MSUALG_4, LATTICES, NAT_LAT, CARD_3, FINSEQ_1, NAT_1, XXREAL_0;
definitions ;
theorems BINOP_1, PBOOLE, MSUALG_4, EQREL_1, TARSKI, NAT_LAT, LATTICES, RELAT_1, RELAT_2, FUNCT_2, CARD_3, ZFMISC_1, MSUALG_1, FUNCT_1, MSUALG_3, FINSEQ_1, NAT_1, MSAFREE2, XBOOLE_0, XBOOLE_1, FINSEQ_3, XCMPLX_1, ORDERS_1, XREAL_1, XXREAL_0, PARTFUN1, FINSEQ_2;
schemes PBOOLE, BINOP_1, NAT_1, FINSEQ_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1, EQREL_1, PBOOLE, STRUCT_0, LATTICES, NAT_LAT, PRALG_1, MSUALG_1, MSUALG_3, MSUALG_4, ORDINAL1, CARD_1, RELAT_2;
constructors HIDDEN, BINOP_1, XXREAL_0, NAT_1, NAT_D, EQREL_1, REALSET1, NAT_LAT, MSUALG_3, MSUALG_4, RELSET_1, PRALG_2, FUNCOP_1, FINSEQ_2;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities BINOP_1, REALSET1, EQREL_1;
expansions ;
definition
let X be
set ;
existence
ex b1 being strict Lattice st
( the carrier of b1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) )
uniqueness
for b1, b2 being strict Lattice st the carrier of b1 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b1 . (x,y) = x /\ y & the L_join of b1 . (x,y) = x "\/" y ) ) & the carrier of b2 = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of b2 . (x,y) = x /\ y & the L_join of b2 . (x,y) = x "\/" y ) ) holds
b1 = b2
end;
definition
let I be non
empty set ;
let M be
ManySortedSet of
I;
existence
ex b1 being strict Lattice st
( ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . (x,y) = x (/\) y & the L_join of b1 . (x,y) = x "\/" y ) ) )
uniqueness
for b1, b2 being strict Lattice st ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . (x,y) = x (/\) y & the L_join of b1 . (x,y) = x "\/" y ) ) & ( for x being set holds
( x in the carrier of b2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b2 . (x,y) = x (/\) y & the L_join of b2 . (x,y) = x "\/" y ) ) holds
b1 = b2
end;
theorem Th13:
for
S being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra over
S for
o being
OperSymbol of
S for
C1,
C2 being
MSCongruence of
A for
C being
MSEquivalence-like ManySortedRelation of
A st
C = C1 "\/" C2 holds
for
x1,
y1 being
object for
n being
Element of
NAT for
a1,
a2,
b1 being
FinSequence st
len a1 = n &
len a1 = len a2 & ( for
k being
Element of
NAT st
k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) &
[((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) &
[x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for
x being
Element of
Args (
o,
A) st
x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)