:: More on the Lattice of Many Sorted Equivalence Relations :: by Robert Milewski :: :: Received February 9, 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 NUMBERS, XBOOLE_0, PBOOLE, REAL_1, STRUCT_0, MSUALG_5, EQREL_1, RELAT_1, FUNCT_1, MSUALG_4, TARSKI, ZFMISC_1, XXREAL_2, SUBSET_1, LATTICES, CLOSURE2, SETFAM_1, FUNCT_4, REWRITE1, LATTICE3, MSSUBFAM, NAT_LAT, REALSET1, XXREAL_0, XXREAL_1, REAL_LAT, BINOP_1, SUPINF_1, ORDINAL2, ARYTM_1, CARD_1, ARYTM_3, MSUALG_7, SETLIM_2, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SUPINF_1, ORDINAL1, FUNCT_7, XXREAL_0, REAL_1, XXREAL_2, XCMPLX_0, XREAL_0, STRUCT_0, RELSET_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, NUMBERS, RCOMP_1, EQREL_1, BINOP_1, REALSET1, PBOOLE, LATTICES, LATTICE3, NAT_LAT, REAL_LAT, MSUALG_3, MSUALG_4, MSUALG_5, SETFAM_1, MSSUBFAM, CLOSURE2; constructors BINOP_1, REAL_1, SQUARE_1, SUPINF_1, RCOMP_1, REALSET1, MSSUBFAM, REAL_LAT, LATTICE3, MSUALG_3, MSUALG_5, CLOSURE2, XXREAL_2, RELSET_1, FUNCT_7; registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, MSSUBFAM, STRUCT_0, LATTICES, LATTICE3, CLOSURE2, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: LATTICE OF MANY SORTED EQUIVALENCE RELATIONS IS COMPLETE reserve I for non empty set; reserve M for ManySortedSet of I; reserve Y,x,y,i for set; reserve r,r1,r2 for Real; theorem :: MSUALG_7:1 id M is Equivalence_Relation of M; theorem :: MSUALG_7:2 [|M,M|] is Equivalence_Relation of M; registration let I,M; cluster EqRelLatt M -> bounded; end; theorem :: MSUALG_7:3 Bottom EqRelLatt M = id M; theorem :: MSUALG_7:4 Top EqRelLatt M = [|M,M|]; theorem :: MSUALG_7:5 for X be Subset of EqRelLatt M holds X is SubsetFamily of [|M,M|]; theorem :: MSUALG_7:6 for a,b be Element of EqRelLatt M, A,B be Equivalence_Relation of M st a = A & b = B holds a [= b iff A c= B; theorem :: MSUALG_7:7 for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st X1 = X for a,b be Equivalence_Relation of M st a = meet |:X1:| & b in X holds a c= b; theorem :: MSUALG_7:8 for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st X1 = X & X is non empty holds meet |:X1:| is Equivalence_Relation of M; definition let L be non empty LattStr; redefine attr L is complete means :: MSUALG_7:def 1 for X being Subset of L ex a being Element of L st X is_less_than a & for b being Element of L st X is_less_than b holds a [= b; end; theorem :: MSUALG_7:9 EqRelLatt M is complete; registration let I,M; cluster EqRelLatt M -> complete; end; theorem :: MSUALG_7:10 for X be Subset of EqRelLatt M, X1 be SubsetFamily of [|M,M|] st X1 = X & X is non empty for a,b be Equivalence_Relation of M st a = meet |:X1:| & b = "/\" (X,EqRelLatt M) holds a = b; begin :: SUBLATTICES INHERITING SUP'S AND INF'S definition let L be Lattice; let IT be SubLattice of L; attr IT is /\-inheriting means :: MSUALG_7:def 2 for X being Subset of IT holds "/\" (X ,L) in the carrier of IT; attr IT is \/-inheriting means :: MSUALG_7:def 3 for X being Subset of IT holds "\/" (X ,L) in the carrier of IT; end; theorem :: MSUALG_7:11 for L be Lattice, L9 be SubLattice of L, a,b be Element of L, a9 ,b9 be Element of L9 st a = a9 & b = b9 holds a "\/" b = a9 "\/" b9 & a "/\" b = a9 "/\" b9; theorem :: MSUALG_7:12 for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be Element of L, a9 be Element of L9 st a = a9 holds a is_less_than X iff a9 is_less_than X; theorem :: MSUALG_7:13 for L be Lattice, L9 be SubLattice of L, X be Subset of L9, a be Element of L, a9 be Element of L9 st a = a9 holds X is_less_than a iff X is_less_than a9; theorem :: MSUALG_7:14 for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting holds L9 is complete; theorem :: MSUALG_7:15 for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting holds L9 is complete; registration let L be complete Lattice; cluster complete for SubLattice of L; end; registration let L be complete Lattice; cluster /\-inheriting -> complete for SubLattice of L; cluster \/-inheriting -> complete for SubLattice of L; end; theorem :: MSUALG_7:16 for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting for A9 be Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9); theorem :: MSUALG_7:17 for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting for A9 be Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9); theorem :: MSUALG_7:18 for L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting for A be Subset of L, A9 be Subset of L9 st A = A9 holds "/\" A = "/\" A9; theorem :: MSUALG_7:19 for L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting for A be Subset of L, A9 be Subset of L9 st A = A9 holds "\/" A = "\/" A9; begin :: SEGMENT OF REAL NUMBERS AS A COMPLETE LATTICE definition let r1,r2 such that r1 <= r2; func RealSubLatt(r1,r2) -> strict Lattice means :: MSUALG_7:def 4 the carrier of it = [.r1,r2.] & the L_join of it = maxreal||[.r1,r2.] & the L_meet of it = minreal ||[.r1,r2.]; end; theorem :: MSUALG_7:20 for r1,r2 st r1 <= r2 holds RealSubLatt(r1,r2) is complete; theorem :: MSUALG_7:21 ex L9 be SubLattice of RealSubLatt(In(0,REAL),In(1,REAL)) st L9 is \/-inheriting non /\-inheriting; theorem :: MSUALG_7:22 ex L be complete Lattice, L9 be SubLattice of L st L9 is \/-inheriting non /\-inheriting; theorem :: MSUALG_7:23 ex L9 be SubLattice of RealSubLatt(In(0,REAL),In(1,REAL)) st L9 is /\-inheriting non \/-inheriting; theorem :: MSUALG_7:24 ex L be complete Lattice, L9 be SubLattice of L st L9 is /\-inheriting non \/-inheriting;