Defining Lattices in MIZAR

There are at least two approaches to lattices in mathematics. According to the first, a lattice is an algebra with two binary operations $\sqcup$ and $\sqcap$ which satisfy the conditions of idempotency, associativity, commutativity, and absorption. According to the second, a lattice is a partially ordered set (poset) with suprema and infima for non empty finite subsets. Both approaches were already present in the MML and the correspondence between them was proved [19,16,1]. The second approach gives wider usage and is easier to generalize (e.g. by weakening the condition of partial ordering). This approach was chosen and the first revision of the MML consisted in generalization of posets and some lattice-theoretical concepts.

RelStr is the base structure of quasi ordered sets, posets, semilattices, and lattices and was introduced in [16] as follows:

 definition
   struct (1-sorted) RelStr (#
     carrier     -> set,
     InternalRel -> Relation of the carrier
   #);
 end;

If $R$ is RelStr then $R$ is a structure with at least 2 fields: carrier and InternatRel. A structure $S$ can be a RelStr and may have more fields when its type is derived from RelStr. This is not the case when $S$ is strict RelStr. The definition of the attribute strict is generated automatically by each structure definition.

The concept of a poset was introduced as follows:

 definition
   mode Poset is reflexive transitive antisymmetric RelStr;
 end;

The attributes reflexive, transitive, and antisymmetric and the following existential cluster registration were introduced earlier.

 definition
   cluster non empty reflexive transitive antisymmetric strict RelStr;
   existence
    proof
     :: Demonstration that such an object exists
    end;
 end;

(Two colons :: start a comment which ends at the end of the line.)

The above cluster assures existence of a RelStr type objects with any subset of the listed attributes.

For convenience and to be closer to usual notation the following definition was introduced.

 definition
   let R be RelStr;
   let x, y be Element of the carrier of R;
   pred x <= y means
 :: ORDERS_1:def 9
    [x,y] in the InternalRel of R;
   synonym y >= x;
 end;

The characterizations of reflexivity, transitivity, and antisymmetry were given in [2] as redefinitions:

 definition
   let A be non empty RelStr;
  redefine
   attr A is reflexive means
 :: YELLOW_0:def 1
     for x being Element of A holds x <= x;
    compatibility proof .... end;
 end;

 definition
   let A be RelStr;
  redefine
   attr A is transitive means
 :: YELLOW_0:def 2
     for x,y,z being Element of A st x <= y & y <= z holds x <= z;
    compatibility proof .... end;
   attr A is antisymmetric means
 :: YELLOW_0:def 3
     for x,y being Element of A st x <= y & y <= x holds x = y;
    compatibility proof .... end;
 end;

The concept of lattice was introduced by definitions:

 definition
   let R be RelStr;
   attr R is with_join means
 :: LATTICE3:def 10
     for x,y being Element of R
      ex z being Element of R st x <= z & y <= z &
       for z' being Element of R st x <= z' & y <= z' holds z <= z';
   attr R is with_meet means
 :: LATTICE3:def 11
     for x,y being Element of R
      ex z being Element of R st z <= x & z <= y &
       for z' being Element of R st z' <= x & z' <= y holds z' <= z;
 end;

 :: WAYBEL_0
 definition
  mode Semilattice is with_meet Poset;
  mode sup-Semilattice is with_join Poset;
  mode LATTICE is with_join with_meet Poset;
 end;