:: More on the Lattice of Congruences in a Many Sorted Algebra :: by Robert Milewski :: :: Received March 6, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, PBOOLE, SUBSET_1, NUMBERS, FINSEQ_1, STRUCT_0, MSUALG_1, RELAT_1, XXREAL_0, ARYTM_3, FUNCT_1, MSUALG_5, EQREL_1, TARSKI, LATTICES, XXREAL_2, REWRITE1, LATTICE3, SETFAM_1, ZFMISC_1, CARD_1, MSUALG_4, CLOSURE2, NAT_1, MARGREL1, PARTFUN1, FUNCT_4, FINSET_1, CARD_3, MSUALG_6, MSUALG_7, MSUALG_8; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, RELSET_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, STRUCT_0, NAT_1, BINOP_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, FINSEQ_1, CARD_3, REWRITE1, EQREL_1, LATTICES, LATTICE3, PBOOLE, MSSUBFAM, MSUALG_1, MSUALG_4, MSUALG_5, CLOSURE2, MSUALG_6, MSUALG_7, XXREAL_0; constructors BINOP_1, NAT_1, MEMBERED, REALSET1, REWRITE1, MSSUBFAM, LATTICE3, MSUALG_5, CLOSURE2, MSUALG_6, MSUALG_7, RELSET_1, NUMBERS; registrations SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, MEMBERED, EQREL_1, PBOOLE, STRUCT_0, LATTICES, MSUALG_1, MSUALG_3, MSUALG_5, CLOSURE2, MSUALG_6, MSUALG_7, FUNCT_1, XXREAL_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin :: MORE ON THE LATTICE OF EQUIVALENCE RELATIONS :: reserve I for non empty set; reserve M for ManySortedSet of I; reserve Y,x,y,y1,i,j for set; reserve k for Element of NAT; reserve p for FinSequence; reserve S for non void non empty ManySortedSign; reserve A for non-empty MSAlgebra over S; theorem :: MSUALG_8:1 for n be Nat, p be FinSequence holds 1 <= n & n < len p iff n in dom p & n+1 in dom p; scheme :: MSUALG_8:sch 1 NonUniqSeqEx{A()->(Element of NAT),P[object,object]}: ex p st dom p = Seg A() & for k st k in Seg A() holds P[k,p.k] provided for k st k in Seg A() ex x being object st P[k,x]; theorem :: MSUALG_8:2 for a,b be Element of EqRelLatt Y for A,B be Equivalence_Relation of Y st a = A & b = B holds a [= b iff A c= B; registration let Y; cluster EqRelLatt Y -> bounded; end; theorem :: MSUALG_8:3 Bottom EqRelLatt Y = id Y; theorem :: MSUALG_8:4 Top EqRelLatt Y = nabla Y; theorem :: MSUALG_8:5 EqRelLatt Y is complete; registration let Y; cluster EqRelLatt Y -> complete; end; theorem :: MSUALG_8:6 for Y be set for X be Subset of EqRelLatt Y holds union X is Relation of Y; theorem :: MSUALG_8:7 for Y be set for X be Subset of EqRelLatt Y holds union X c= "\/" X; theorem :: MSUALG_8:8 for Y be set for X be Subset of EqRelLatt Y for R be Relation of Y st R = union X holds "\/" X = EqCl R; theorem :: MSUALG_8:9 for Y be set for X be Subset of EqRelLatt Y for R be Relation st R = union X holds R = R~; theorem :: MSUALG_8:10 for Y be set for X be Subset of EqRelLatt Y holds x in Y & y in Y implies ( [x,y] in "\/" X iff ex f being FinSequence st 1 <= len f & x = f.1 & y = f.(len f) & for i be Nat st 1 <= i & i < len f holds [f.i,f.(i +1)] in union X ); begin :: Lattice of Congruences in a Many Sorted Algebra as a Sublattice :: of Lattice of Many Sorted Equivalence Relations Inheriting Sups and Infs theorem :: MSUALG_8:11 for B be Subset of CongrLatt A holds "/\" (B,EqRelLatt the Sorts of A) is MSCongruence of A; definition let S,A; 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); end; definition let S,A; 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); end; theorem :: MSUALG_8:12 for C be Element of EqRelLatt the Sorts of A st C is MSCongruence of A holds CongrCl C = C; theorem :: MSUALG_8:13 for X be Subset of EqRelLatt the Sorts of A holds CongrCl "\/" (X, EqRelLatt the Sorts of A) = CongrCl X; theorem :: MSUALG_8:14 for B1,B2 be Subset of CongrLatt A, C1,C2 be 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); theorem :: MSUALG_8:15 for X be 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); theorem :: MSUALG_8:16 for i be Element of I for e be Equivalence_Relation of M.i ex E be Equivalence_Relation of M st E.i = e & for j be Element of I st j <> i holds E.j = nabla (M.j); 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(X,i); end; 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; redefine func EqRelSet (X,i) -> Subset of EqRelLatt M.i means :: MSUALG_8:def 3 x in it iff ex Eq be Equivalence_Relation of M st x = Eq.i & Eq in X; end; theorem :: MSUALG_8:17 for i be Element of S for X be Subset of EqRelLatt the Sorts of A for B be Equivalence_Relation of the Sorts of A st B = "\/" X holds B.i = "\/" (EqRelSet (X,i) , EqRelLatt (the Sorts of A).i); theorem :: MSUALG_8:18 for X be Subset of CongrLatt A holds "\/" (X,EqRelLatt the Sorts of A) is MSCongruence of A; theorem :: MSUALG_8:19 CongrLatt A is /\-inheriting; theorem :: MSUALG_8:20 CongrLatt A is \/-inheriting; registration let S,A; cluster CongrLatt A -> /\-inheriting \/-inheriting; end;