:: Lattice of Congruences in a Many Sorted Algebra
:: by Robert Milewski
::
:: Received January 11, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: MSUALG_5:1
canceled;
:: deftheorem Def1 defines EqCl MSUALG_5:def 1 :
theorem Th2: :: MSUALG_5:2
theorem Th3: :: MSUALG_5:3
theorem :: MSUALG_5:4
canceled;
definition
let X be
set ;
func EqRelLatt X -> strict Lattice means :: MSUALG_5:def 2
( the
carrier of
it = { 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
it . x,
y = x /\ y & the
L_join of
it . x,
y = x "\/" y ) ) );
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;
:: deftheorem defines EqRelLatt MSUALG_5:def 2 :
:: deftheorem Def3 defines EqCl MSUALG_5:def 3 :
theorem :: MSUALG_5:5
:: deftheorem Def4 defines "\/" MSUALG_5:def 4 :
theorem Th6: :: MSUALG_5:6
theorem Th7: :: MSUALG_5:7
theorem Th8: :: MSUALG_5:8
theorem :: MSUALG_5:9
theorem Th10: :: MSUALG_5:10
theorem Th11: :: MSUALG_5:11
theorem Th12: :: MSUALG_5:12
theorem Th13: :: MSUALG_5:13
definition
let I be non
empty set ;
let M be
ManySortedSet of
I;
func EqRelLatt M -> strict Lattice means :
Def5:
:: MSUALG_5:def 5
( ( for
x being
set holds
(
x in the
carrier of
it iff
x is
Equivalence_Relation of
M ) ) & ( for
x,
y being
Equivalence_Relation of
M holds
( the
L_meet of
it . x,
y = x /\ y & the
L_join of
it . x,
y = x "\/" y ) ) );
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;
:: deftheorem Def5 defines EqRelLatt MSUALG_5:def 5 :
theorem Th14: :: MSUALG_5:14
theorem Th15: :: MSUALG_5:15
for
S being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra of
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
set 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)
theorem Th16: :: MSUALG_5:16
theorem Th17: :: MSUALG_5:17
theorem Th18: :: MSUALG_5:18
:: deftheorem Def6 defines CongrLatt MSUALG_5:def 6 :
theorem Th19: :: MSUALG_5:19
theorem Th20: :: MSUALG_5:20
theorem :: MSUALG_5:21
theorem :: MSUALG_5:22