Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

### More on the Lattice of Many Sorted Equivalence Relations

**by****Robert Milewski**- Received February 9, 1996
- MML identifier: MSUALG_7

- [ Mizar article, MML identifier index ]

environ vocabulary PBOOLE, MSUALG_5, EQREL_1, RELAT_1, FUNCT_1, MSUALG_4, PRALG_2, LATTICES, BOOLE, CLOSURE2, MSUALG_2, SETFAM_1, FUNCT_4, CANTOR_1, ZF_REFLE, BHSP_3, LATTICE3, MSSUBFAM, NAT_LAT, RCOMP_1, REAL_LAT, SQUARE_1, BINOP_1, SUPINF_1, ORDINAL2, ARYTM_3, ARYTM_1, SEQ_2, MSUALG_7; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, SUPINF_1, REAL_1, SQUARE_1, STRUCT_0, RELSET_1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, RCOMP_1, EQREL_1, BINOP_1, PBOOLE, LATTICES, LATTICE3, NAT_LAT, REAL_LAT, PRALG_2, MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_5, CANTOR_1, SETFAM_1, MSSUBFAM, CLOSURE2; constructors DOMAIN_1, SUPINF_1, SQUARE_1, REAL_1, BINOP_1, LATTICE3, REAL_LAT, RCOMP_1, MSUALG_3, MSUALG_5, CANTOR_1, CLOSURE2, MEMBERED, MSSUBFAM; clusters SUBSET_1, STRUCT_0, LATTICE3, SUPINF_1, MSSUBFAM, CLOSURE2, LATTICES, XREAL_0, RELSET_1, XBOOLE_0, MEMBERED; 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 for X be set holds x in the carrier of EqRelLatt X iff x is Equivalence_Relation of X; theorem :: MSUALG_7:2 id M is Equivalence_Relation of M; theorem :: MSUALG_7:3 [|M,M|] is Equivalence_Relation of M; definition let I,M; cluster EqRelLatt M -> bounded; end; theorem :: MSUALG_7:4 Bottom EqRelLatt M = id M; theorem :: MSUALG_7:5 Top EqRelLatt M = [|M,M|]; theorem :: MSUALG_7:6 for X be Subset of EqRelLatt M holds X is SubsetFamily of [|M,M|]; theorem :: MSUALG_7:7 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:8 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:9 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:10 EqRelLatt M is complete; definition let I,M; cluster EqRelLatt M -> complete; end; theorem :: MSUALG_7:11 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:12 for L be Lattice, L' be SubLattice of L, a,b be Element of L, a',b' be Element of L' st a = a' & b = b' holds ( a "\/" b = a' "\/" b' & a "/\" b = a' "/\" b' ); theorem :: MSUALG_7:13 for L be Lattice, L' be SubLattice of L, X be Subset of L', a be Element of L, a' be Element of L' st a = a' holds a is_less_than X iff a' is_less_than X; theorem :: MSUALG_7:14 for L be Lattice, L' be SubLattice of L, X be Subset of L', a be Element of L, a' be Element of L' st a = a' holds X is_less_than a iff X is_less_than a'; theorem :: MSUALG_7:15 for L be complete Lattice, L' be SubLattice of L st L' is /\-inheriting holds L' is complete; theorem :: MSUALG_7:16 for L be complete Lattice, L' be SubLattice of L st L' is \/-inheriting holds L' is complete; definition let L be complete Lattice; cluster complete SubLattice of L; end; definition let L be complete Lattice; cluster /\-inheriting -> complete SubLattice of L; cluster \/-inheriting -> complete SubLattice of L; end; theorem :: MSUALG_7:17 for L be complete Lattice, L' be SubLattice of L st L' is /\-inheriting for A' be Subset of L' holds "/\" (A',L) = "/\" (A',L'); theorem :: MSUALG_7:18 for L be complete Lattice, L' be SubLattice of L st L' is \/-inheriting for A' be Subset of L' holds "\/" (A',L) = "\/" (A',L'); theorem :: MSUALG_7:19 for L be complete Lattice, L' be SubLattice of L st L' is /\-inheriting for A be Subset of L, A' be Subset of L' st A = A' holds "/\" A = "/\" A'; theorem :: MSUALG_7:20 for L be complete Lattice, L' be SubLattice of L st L' is \/-inheriting for A be Subset of L, A' be Subset of L' st A = A' holds "\/" A = "\/" A'; 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.],[.r1,r2.]:] qua set) & the L_meet of it = minreal|([:[.r1,r2.],[.r1,r2.]:] qua set); end; theorem :: MSUALG_7:21 for r1,r2 st r1 <= r2 holds RealSubLatt(r1,r2) is complete; theorem :: MSUALG_7:22 ex L' be SubLattice of RealSubLatt(0,1) st L' is \/-inheriting non /\-inheriting; theorem :: MSUALG_7:23 ex L be complete Lattice, L' be SubLattice of L st L' is \/-inheriting non /\-inheriting; theorem :: MSUALG_7:24 ex L' be SubLattice of RealSubLatt(0,1) st L' is /\-inheriting non \/-inheriting; theorem :: MSUALG_7:25 ex L be complete Lattice, L' be SubLattice of L st L' is /\-inheriting non \/-inheriting;

Back to top