:: by Robert Milewski

::

:: Received March 6, 1996

:: Copyright (c) 1996-2018 Association of Mizar Users

theorem Th1: :: MSUALG_8:1

for n being Nat

for p being FinSequence holds

( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) )

for p being FinSequence holds

( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) )

proof end;

theorem Th2: :: MSUALG_8:2

for Y being set

for a, b being Element of (EqRelLatt Y)

for A, B being Equivalence_Relation of Y st a = A & b = B holds

( a [= b iff A c= B )

for a, b being Element of (EqRelLatt Y)

for A, B being Equivalence_Relation of Y st a = A & b = B holds

( a [= b iff A c= B )

proof end;

registration
end;

registration
end;

theorem Th8: :: MSUALG_8:8

for Y being set

for X being Subset of (EqRelLatt Y)

for R being Relation of Y st R = union X holds

"\/" X = EqCl R

for X being Subset of (EqRelLatt Y)

for R being Relation of Y st R = union X holds

"\/" X = EqCl R

proof end;

theorem Th9: :: MSUALG_8:9

for Y being set

for X being Subset of (EqRelLatt Y)

for R being Relation st R = union X holds

R = R ~

for X being Subset of (EqRelLatt Y)

for R being Relation st R = union X holds

R = R ~

proof end;

theorem Th10: :: MSUALG_8:10

for x, y, Y being set

for X being Subset of (EqRelLatt Y) st x in Y & y in Y holds

( [x,y] in "\/" X iff ex f being FinSequence st

( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds

[(f . i),(f . (i + 1))] in union X ) ) )

for X being Subset of (EqRelLatt Y) st x in Y & y in Y holds

( [x,y] in "\/" X iff ex f being FinSequence st

( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds

[(f . i),(f . (i + 1))] in union X ) ) )

proof end;

:: of Lattice of Many Sorted Equivalence Relations Inheriting Sups and Infs

theorem Th11: :: MSUALG_8:11

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A

for A being non-empty MSAlgebra over S

for B being Subset of (CongrLatt A) holds "/\" (B,(EqRelLatt the Sorts of A)) is MSCongruence of A

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let E be Element of (EqRelLatt the Sorts of A);

"/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A

end;
let A be non-empty MSAlgebra over S;

let E be Element of (EqRelLatt the Sorts of A);

func CongrCl E -> MSCongruence of A equals :: MSUALG_8:def 1

"/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A));

coherence "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A));

"/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A

proof end;

:: deftheorem defines CongrCl MSUALG_8:def 1 :

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for E being Element of (EqRelLatt the Sorts of A) holds CongrCl E = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A));

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for E being Element of (EqRelLatt the Sorts of A) holds CongrCl E = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A));

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let X be Subset of (EqRelLatt the Sorts of A);

"/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A

end;
let A be non-empty MSAlgebra over S;

let X be Subset of (EqRelLatt the Sorts of A);

func CongrCl X -> MSCongruence of A equals :: MSUALG_8:def 2

"/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A));

coherence "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A));

"/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A)) is MSCongruence of A

proof end;

:: deftheorem defines CongrCl MSUALG_8:def 2 :

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl X = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A));

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl X = "/\" ( { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A));

theorem :: MSUALG_8:12

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds

CongrCl C = C

for A being non-empty MSAlgebra over S

for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds

CongrCl C = C

proof end;

theorem :: MSUALG_8:13

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X

for A being non-empty MSAlgebra over S

for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" (X,(EqRelLatt the Sorts of A))) = CongrCl X

proof end;

theorem :: MSUALG_8:14

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for B1, B2 being Subset of (CongrLatt A)

for C1, C2 being MSCongruence of A st C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) holds

C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A))

for A being non-empty MSAlgebra over S

for B1, B2 being Subset of (CongrLatt A)

for C1, C2 being MSCongruence of A st C1 = "\/" (B1,(EqRelLatt the Sorts of A)) & C2 = "\/" (B2,(EqRelLatt the Sorts of A)) holds

C1 "\/" C2 = "\/" ((B1 \/ B2),(EqRelLatt the Sorts of A))

proof end;

theorem :: MSUALG_8:15

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A))

for A being non-empty MSAlgebra over S

for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) = "\/" ( { ("\/" (X0,(EqRelLatt the Sorts of A))) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A))

proof end;

theorem Th16: :: MSUALG_8:16

for I being non empty set

for M being ManySortedSet of I

for i being Element of I

for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st

( E . i = e & ( for j being Element of I st j <> i holds

E . j = nabla (M . j) ) )

for M being ManySortedSet of I

for i being Element of I

for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st

( E . i = e & ( for j being Element of I st j <> i holds

E . j = nabla (M . j) ) )

proof end;

notation

let I be non empty set ;

let M be ManySortedSet of I;

let i be Element of I;

let X be Subset of (EqRelLatt M);

synonym EqRelSet (X,i) for pi (M,I);

end;
let M be ManySortedSet of I;

let i be Element of I;

let X be Subset of (EqRelLatt M);

synonym EqRelSet (X,i) for pi (M,I);

definition

let I be non empty set ;

let M be ManySortedSet of I;

let i be Element of I;

let X be Subset of (EqRelLatt M);

EqRelSet (,) is Subset of (EqRelLatt (M . i))

for b_{1} being Subset of (EqRelLatt (M . i)) holds

( b_{1} = EqRelSet (,) iff for x being set holds

( x in b_{1} iff ex Eq being Equivalence_Relation of M st

( x = Eq . i & Eq in X ) ) )

end;
let M be ManySortedSet of I;

let i be Element of I;

let X be Subset of (EqRelLatt M);

:: original: EqRelSet

redefine func EqRelSet (X,i) -> Subset of (EqRelLatt (M . i)) means :Def3: :: MSUALG_8:def 3

for x being set holds

( x in it iff ex Eq being Equivalence_Relation of M st

( x = Eq . i & Eq in X ) );

coherence redefine func EqRelSet (X,i) -> Subset of (EqRelLatt (M . i)) means :Def3: :: MSUALG_8:def 3

for x being set holds

( x in it iff ex Eq being Equivalence_Relation of M st

( x = Eq . i & Eq in X ) );

EqRelSet (,) is Subset of (EqRelLatt (M . i))

proof end;

compatibility for b

( b

( x in b

( x = Eq . i & Eq in X ) ) )

proof end;

:: deftheorem Def3 defines EqRelSet MSUALG_8:def 3 :

for I being non empty set

for M being ManySortedSet of I

for i being Element of I

for X being Subset of (EqRelLatt M)

for b_{5} being Subset of (EqRelLatt (M . i)) holds

( b_{5} = EqRelSet (X,i) iff for x being set holds

( x in b_{5} iff ex Eq being Equivalence_Relation of M st

( x = Eq . i & Eq in X ) ) );

for I being non empty set

for M being ManySortedSet of I

for i being Element of I

for X being Subset of (EqRelLatt M)

for b

( b

( x in b

( x = Eq . i & Eq in X ) ) );

theorem Th17: :: MSUALG_8:17

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for i being Element of S

for X being Subset of (EqRelLatt the Sorts of A)

for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds

B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))

for A being non-empty MSAlgebra over S

for i being Element of S

for X being Subset of (EqRelLatt the Sorts of A)

for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds

B . i = "\/" ((EqRelSet (X,i)),(EqRelLatt ( the Sorts of A . i)))

proof end;

theorem Th18: :: MSUALG_8:18

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S

for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) is MSCongruence of A

for A being non-empty MSAlgebra over S

for X being Subset of (CongrLatt A) holds "\/" (X,(EqRelLatt the Sorts of A)) is MSCongruence of A

proof end;

theorem Th19: :: MSUALG_8:19

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S holds CongrLatt A is /\-inheriting

for A being non-empty MSAlgebra over S holds CongrLatt A is /\-inheriting

proof end;

theorem Th20: :: MSUALG_8:20

for S being non empty non void ManySortedSign

for A being non-empty MSAlgebra over S holds CongrLatt A is \/-inheriting

for A being non-empty MSAlgebra over S holds CongrLatt A is \/-inheriting

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

coherence

( CongrLatt A is /\-inheriting & CongrLatt A is \/-inheriting ) by Th19, Th20;

end;
let A be non-empty MSAlgebra over S;

coherence

( CongrLatt A is /\-inheriting & CongrLatt A is \/-inheriting ) by Th19, Th20;