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;