The Mizar article:

The Lattice of Real Numbers. The Lattice of Real Functions

by
Marek Chmur

Received May 22, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: REAL_LAT
[ MML identifier index ]


environ

 vocabulary BINOP_1, FUNCT_1, SQUARE_1, LATTICES, ARYTM, FUNCT_2, RELAT_1,
      QC_LANG1, REAL_LAT;
 notation XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, SQUARE_1, STRUCT_0,
      LATTICES, BINOP_1, FUNCSDOM, RELAT_1, FUNCT_2, FRAENKEL;
 constructors SQUARE_1, LATTICES, FUNCSDOM, MEMBERED, XBOOLE_0;
 clusters LATTICES, RLSUB_2, RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions LATTICES;
 theorems SQUARE_1, LATTICES, BINOP_1, FUNCT_2, FUNCOP_1, XREAL_0;
 schemes BINOP_1;

begin :: LATTICE of REAL NUMBERS

reserve x,y for Real;

definition
 func minreal-> BinOp of REAL means
 :Def1: it.(x,y)=min(x,y);
 existence
  proof
    deffunc O(Element of REAL,Element of REAL)=min($1,$2);
    ex o being BinOp of REAL st
    for a,b being Element of REAL holds o.(a,b) = O(a,b) from BinOpLambda;
    hence thesis;
  end;
 uniqueness
  proof
  let f1,f2 be BinOp of REAL;
  assume that
  A1: f1.(x,y)=min(x,y) and
  A2: f2.(x,y)=min(x,y);
    for x,y being Element of REAL holds f1.(x,y)=f2.(x,y)
    proof
    let x,y be Element of REAL;
      f1.(x,y)=min(x,y) & f2.(x,y)=min(x,y) by A1,A2;
    hence thesis;
   end;
  hence thesis by BINOP_1:2;
  end;

 func maxreal-> BinOp of REAL means
 :Def2: it.(x,y)=max(x,y);
 existence
  proof
    deffunc O(Element of REAL,Element of REAL)=max($1,$2);
    ex o being BinOp of REAL st
    for a,b being Element of REAL holds o.(a,b) = O(a,b) from BinOpLambda;
    hence thesis;
  end;
 uniqueness
  proof
  let f1,f2 be BinOp of REAL;
  assume that
  A3: f1.(x,y)=max(x,y) and
  A4: f2.(x,y)=max(x,y);
    for x,y being Element of REAL holds f1.(x,y)=f2.(x,y)
    proof
    let x,y be Element of REAL;
      f1.(x,y)=max(x,y) & f2.(x,y)=max(x,y) by A3,A4;
    hence thesis;
   end;
  hence thesis by BINOP_1:2;
  end;
end;

definition
 canceled;

 func Real_Lattice -> strict LattStr equals
 :Def4: LattStr (# REAL, maxreal, minreal #);
 coherence;
end;

definition
 cluster -> real Element of Real_Lattice;
 coherence by Def4,XREAL_0:def 1;
end;

definition
 cluster Real_Lattice -> non empty;
 coherence by Def4;
end;

reserve p,q,a,b,c for Element of Real_Lattice;

Lm1: p"\/"q = max(p,q)
 proof
    p"\/"q = maxreal.(p,q) by Def4,LATTICES:def 1;
  hence p"\/"q=max(p,q) by Def2,Def4;
 end;

Lm2: p"/\"q = min(p,q)
 proof
     p"/\"q = minreal.(p,q) by Def4,LATTICES:def 2;
  hence p"/\"q=min(p,q) by Def1,Def4;
 end;

Lm3: a"\/"b = b"\/"a
 proof
  thus a"\/"b = max(a,b) by Lm1
           .= b"\/"a by Lm1;
 end;

Lm4: a"\/"(b"\/"c) = (a"\/"b)"\/"c
 proof
 set l=b"\/"c;
 A1: a"\/"(b"\/"c) =max(a,l) by Lm1;
   max(b,c)=l by Lm1;
 then A2: a"\/"(b"\/"c)=max(max(a,b),c) by A1,SQUARE_1:51;
    max(a,b)=a"\/"b by Lm1;
 hence thesis by A2,Lm1;
 end;

Lm5: (a"/\"b)"\/"b = b
 proof
  set k=a"/\"b;
    min(a,b)=k by Lm2;
 hence (a"/\"b)"\/"b = max(min(a,b),b) by Lm1
               .= b by SQUARE_1:54;
 end;

Lm6: a"/\"b = b"/\"a
 proof
  thus a"/\"b = min(a,b) by Lm2
           .= b"/\"a by Lm2;
 end;

Lm7: a"/\"(b"/\"c) = (a"/\"b)"/\"c
 proof
  set l=b"/\"c;
  set k=a"/\"b;
  A1:min(b,c)=l by Lm2;
  A2:min(a,b)=k by Lm2;
  thus a"/\"(b"/\"c) = min(a,min(b,c)) by A1,Lm2
                .= min(k,c) by A2,SQUARE_1:40
                .= (a"/\"b)"/\"c by Lm2;
 end;

Lm8: a"/\"(a"\/"b) = a
 proof
  set l=a"\/"b;
    max(a,b)=l by Lm1;
  hence a"/\"(a"\/"b) = min(a,max(a,b)) by Lm2
                .= a by SQUARE_1:55;
 end;

definition
 cluster Real_Lattice -> Lattice-like;
 coherence
  proof
        Real_Lattice is join-commutative join-associative meet-absorbing
         meet-commutative meet-associative join-absorbing
         by Lm3,Lm4,Lm5,Lm6,Lm7,Lm8,LATTICES:def 4,def 5,def 6,def 7,def 8,def
9;
      hence thesis by LATTICES:def 10;
  end;
end;

Lm9: a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c)
  proof
  set l=a"/\"c;
  set k=a"/\"b;
  set m=b"\/"c;
  A1:min(a,c)=l by Lm2;
  A2:min(a,b)=k by Lm2;
    max(b,c)=m by Lm1;
  hence a"/\"(b"\/"c) = min(a,max(b,c)) by Lm2
                .= max(k,l) by A1,A2,SQUARE_1:56
                .= (a"/\"b)"\/"(a"/\"c) by Lm1;
 end;

reserve p,q,r for Element of Real_Lattice;

canceled 7;

theorem Th8:
 maxreal.(p,q) = maxreal.(q,p)
 proof
 thus maxreal.(p,q) = q"\/"p by Def4,LATTICES:def 1
                   .= maxreal.(q,p) by Def4,LATTICES:def 1;
 end;

theorem Th9:
 minreal.(p,q) = minreal.(q,p)
 proof
 thus minreal.(p,q) = q"/\"p by Def4,LATTICES:def 2
                   .= minreal.(q,p) by Def4,LATTICES:def 2;
 end;

theorem Th10:
 maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(q,r)),p) &
 maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(p,q)),r) &
 maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(q,p)),r) &
 maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(r,p)),q) &
 maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(r,q)),p) &
 maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(p,r)),q)
 proof
 set s=q"\/"r;
 thus A1:maxreal.(p,(maxreal.(q,r)))=maxreal.(p,s) by Def4,LATTICES:def 1
                   .= s"\/"p by Def4,LATTICES:def 1
                   .= maxreal.(s,p) by Def4,LATTICES:def 1
                   .= maxreal.((maxreal.(q,r)),p) by Def4,LATTICES:def 1;
 thus maxreal.(p,(maxreal.(q,r)))=maxreal.(p,s) by Def4,LATTICES:def 1
                   .= p"\/"s by Def4,LATTICES:def 1
                   .= (p"\/"q)"\/"r by Lm4
                   .= maxreal.(p"\/"q,r) by Def4,LATTICES:def 1
                   .= maxreal.(maxreal.(p,q),r) by Def4,LATTICES:def 1;
 thus maxreal.(p,(maxreal.(q,r)))=maxreal.(p,s) by Def4,LATTICES:def 1
                   .= p"\/"s by Def4,LATTICES:def 1
                   .= (q"\/"p)"\/"r by Lm4
                   .= maxreal.(q"\/"p,r) by Def4,LATTICES:def 1
                   .= maxreal.(maxreal.(q,p),r) by Def4,LATTICES:def 1;
 thus A2:maxreal.(p,(maxreal.(q,r)))=maxreal.(p,s) by Def4,LATTICES:def 1
                   .= p"\/"(r"\/"q) by Def4,LATTICES:def 1
                   .= (r"\/"p)"\/"q by Lm4
                   .= maxreal.(r"\/"p,q) by Def4,LATTICES:def 1
                   .= maxreal.(maxreal.(r,p),q) by Def4,LATTICES:def 1;
 thus maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(r,q)),p) by A1,Th8;
 thus maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(p,r)),q) by A2,Th8;
end;

theorem Th11:
 minreal.(p,(minreal.(q,r)))=minreal.((minreal.(q,r)),p) &
 minreal.(p,(minreal.(q,r)))=minreal.((minreal.(p,q)),r) &
 minreal.(p,(minreal.(q,r)))=minreal.((minreal.(q,p)),r) &
 minreal.(p,(minreal.(q,r)))=minreal.((minreal.(r,p)),q) &
 minreal.(p,(minreal.(q,r)))=minreal.((minreal.(r,q)),p) &
 minreal.(p,(minreal.(q,r)))=minreal.((minreal.(p,r)),q)
 proof
 set s=q"/\"r;
 thus A1:minreal.(p,(minreal.(q,r)))=minreal.(p,s) by Def4,LATTICES:def 2
                   .= s"/\"p by Def4,LATTICES:def 2
                   .= minreal.(s,p) by Def4,LATTICES:def 2
                   .= minreal.((minreal.(q,r)),p) by Def4,LATTICES:def 2;
 thus minreal.(p,(minreal.(q,r)))=minreal.(p,s) by Def4,LATTICES:def 2
                   .= p"/\"s by Def4,LATTICES:def 2
                   .= (p"/\"q)"/\"r by Lm7
                   .= minreal.(p"/\"q,r) by Def4,LATTICES:def 2
                   .= minreal.(minreal.(p,q),r) by Def4,LATTICES:def 2;
 thus minreal.(p,(minreal.(q,r)))=minreal.(p,s) by Def4,LATTICES:def 2
                   .= p"/\"s by Def4,LATTICES:def 2
                   .= (q"/\"p)"/\"r by Lm7
                   .= minreal.(q"/\"p,r) by Def4,LATTICES:def 2
                   .= minreal.(minreal.(q,p),r) by Def4,LATTICES:def 2;
 thus A2:minreal.(p,(minreal.(q,r)))=minreal.(p,s) by Def4,LATTICES:def 2
                   .= p"/\"(r"/\"q) by Def4,LATTICES:def 2
                   .= (r"/\"p)"/\"q by Lm7
                   .= minreal.(r"/\"p,q) by Def4,LATTICES:def 2
                   .= minreal.(minreal.(r,p),q) by Def4,LATTICES:def 2;
 thus minreal.(p,(minreal.(q,r)))=minreal.((minreal.(r,q)),p) by A1,Th9;
 thus minreal.(p,(minreal.(q,r)))=minreal.((minreal.(p,r)),q) by A2,Th9;
end;

theorem Th12:
 maxreal.(minreal.(p,q),q)=q & maxreal.(q,minreal.(p,q))=q &
  maxreal.(q,minreal.(q,p))=q & maxreal.(minreal.(q,p),q)=q
 proof
 set s=p"/\"q;
 thus A1:maxreal.(minreal.(p,q),q)=maxreal.(s,q) by Def4,LATTICES:def 2
                              .=s"\/"q by Def4,LATTICES:def 1
                              .=q by Lm5;
 thus maxreal.(q,minreal.(p,q))=maxreal.(q,s) by Def4,LATTICES:def 2
                              .=(p"/\"q)"\/"q by Def4,LATTICES:def 1
                              .=q by Lm5;
 thus maxreal.(q,minreal.(q,p))=maxreal.(q,q"/\"p) by Def4,LATTICES:def 2
                              .=(p"/\"q)"\/"q by Def4,LATTICES:def 1
                              .=q by Lm5;
 thus maxreal.(minreal.(q,p),q)=q by A1,Th9;
 end;

theorem Th13:
 minreal.(q,maxreal.(q,p))=q & minreal.(maxreal.(p,q),q)=q &
 minreal.(q,maxreal.(p,q))=q & minreal.(maxreal.(q,p),q)=q
 proof
 set s=q"\/"p;
 thus A1:minreal.(q,maxreal.(q,p))=minreal.(q,s) by Def4,LATTICES:def 1
                              .=q"/\"s by Def4,LATTICES:def 2
                              .=q by Lm8;
 thus A2:minreal.(maxreal.(p,q),q)=minreal.(p"\/"q,q) by Def4,LATTICES:def 1
                              .=q"/\"(q"\/"p) by Def4,LATTICES:def 2
                              .=q by Lm8;
 thus minreal.(q,maxreal.(p,q))=q by A1,Th8;
 thus minreal.(maxreal.(q,p),q)=q by A2,Th8;
end;

theorem Th14:
 minreal.(q,maxreal.(p,r))=maxreal.(minreal.(q,p),minreal.(q,r))
 proof
 set s=p"\/"r;
 set w=q"/\"r;
 thus minreal.(q,maxreal.(p,r))=minreal.(q,s) by Def4,LATTICES:def 1
              .=q"/\"s by Def4,LATTICES:def 2
              .=(q"/\"p)"\/"(q"/\"r) by Lm9
              .=maxreal.(q"/\"p,w) by Def4,LATTICES:def 1
              .=maxreal.(minreal.(q,p),w) by Def4,LATTICES:def 2
              .=maxreal.(minreal.(q,p),minreal.(q,r)) by Def4,LATTICES:def 2;
end;


definition
  cluster Real_Lattice -> distributive;
  coherence by Lm9,LATTICES:def 11;
end;

 reserve A,B for non empty set;
 reserve f,g,h for Element of Funcs(A,REAL);

definition let A;
 func maxfuncreal(A) -> BinOp of Funcs(A,REAL) means
 :Def5: it.(f,g) = maxreal.:(f,g);
 existence
  proof
    deffunc O(Element of Funcs(A,REAL),Element of Funcs(A,REAL))
             = maxreal.:($1,$2);
    ex o being BinOp of Funcs(A,REAL) st
    for a,b being Element of Funcs(A,REAL) holds
         o.(a,b) = O(a,b) from BinOpLambda;
    hence thesis;
  end;
 uniqueness
  proof
   let F1,F2 be BinOp of Funcs(A,REAL) such that
   A1: for f,g being Element of Funcs(A,REAL)
       holds F1.(f,g) = maxreal.:(f,g) and
   A2: for f,g being Element of Funcs(A,REAL)
       holds F2.(f,g) = maxreal.:(f,g);
     now
     let f,g be Element of Funcs(A,REAL);
     thus F1.(f,g) = maxreal.:(f,g) by A1
                  .= F2.(f,g) by A2;
   end;
   hence thesis by BINOP_1:2;
  end;

 func minfuncreal(A) -> BinOp of Funcs(A,REAL) means
 :Def6: it.(f,g) = minreal.:(f,g);
 existence
  proof
    deffunc O(Element of Funcs(A,REAL),Element of Funcs(A,REAL))
             = minreal.:($1,$2);
    ex o being BinOp of Funcs(A,REAL) st
    for a,b being Element of Funcs(A,REAL) holds
         o.(a,b) = O(a,b) from BinOpLambda;
    hence thesis;
  end;
 uniqueness
  proof
   let F1,F2 be BinOp of Funcs(A,REAL) such that
   A3: for f,g being Element of Funcs(A,REAL)
       holds F1.(f,g) = minreal.:(f,g) and
   A4: for f,g being Element of Funcs(A,REAL)
       holds F2.(f,g) = minreal.:(f,g);
     now
     let f,g be Element of Funcs(A,REAL);
     thus F1.(f,g) = minreal.:(f,g) by A3
                  .= F2.(f,g) by A4;
   end;
   hence thesis by BINOP_1:2;
  end;
end;

Lm10: for x being Element of A,
        f being Function of A,B holds x in dom f
  proof
  let x be Element of A,f be Function of A,B;
     x in A;
   hence x in dom f by FUNCT_2:def 1;
  end;

canceled 5;

theorem Th20:
 (maxfuncreal(A)).(f,g) = (maxfuncreal(A)).(g,f)
 proof
    now let x be Element of A;
 A1: x in dom (maxreal.:(f,g)) by Lm10;
 A2: x in dom (maxreal.:(g,f)) by Lm10;
 thus
    ((maxfuncreal(A)).(f,g)).x = (maxreal.:(f,g)).x by Def5
                            .= maxreal.(f.x,g.x) by A1,FUNCOP_1:28
                            .= maxreal.(g.x,f.x) by Def4,Th8
                            .= (maxreal.:(g,f)).x by A2,FUNCOP_1:28
                            .= ((maxfuncreal(A)).(g,f)).x by Def5;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem Th21:
 (minfuncreal(A)).(f,g) = (minfuncreal(A)).(g,f)
 proof
    now let x be Element of A;
 A1: x in dom (minreal.:(f,g)) by Lm10;
 A2: x in dom (minreal.:(g,f)) by Lm10;
 thus
    ((minfuncreal(A)).(f,g)).x = (minreal.:(f,g)).x by Def6
                            .= minreal.(f.x,g.x) by A1,FUNCOP_1:28
                            .= minreal.(g.x,f.x) by Def4,Th9
                            .= (minreal.:(g,f)).x by A2,FUNCOP_1:28
                            .= ((minfuncreal(A)).(g,f)).x by Def6;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem Th22:
 (maxfuncreal(A)).((maxfuncreal(A)).(f,g),h)
                       =(maxfuncreal(A)).(f,(maxfuncreal(A)).(g,h))
 proof
    now let x be Element of A;
 A1: x in dom (maxreal.:(f,g)) by Lm10;
 A2: x in dom (maxreal.:(g,h)) by Lm10;
 A3: x in dom (maxreal.:(f,(maxreal.:(g,h)))) by Lm10;
 A4: x in dom (maxreal.:((maxreal.:(f,g)),h)) by Lm10;
 thus ((maxfuncreal(A)).((maxfuncreal(A)).(f,g),h)).x
           =((maxfuncreal(A)).(maxreal.:(f,g),h)).x by Def5
          .=(maxreal.:(maxreal.:(f,g),h)).x by Def5
          .=maxreal.((maxreal.:(f,g)).x,h.x) by A4,FUNCOP_1:28
          .=maxreal.(maxreal.(f.x,g.x),h.x) by A1,FUNCOP_1:28
          .=maxreal.(f.x,maxreal.(g.x,h.x)) by Def4,Th10
          .=maxreal.(f.x,((maxreal.:(g,h)).x)) by A2,FUNCOP_1:28
          .=(maxreal.:(f,(maxreal.:(g,h)))).x by A3,FUNCOP_1:28
          .=((maxfuncreal(A)).(f,(maxreal.:(g,h)))).x by Def5
          .=((maxfuncreal(A)).(f,((maxfuncreal(A)).(g,h)))).x by Def5;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem Th23:
 (minfuncreal(A)).((minfuncreal(A)).(f,g),h)
                       =(minfuncreal(A)).(f,(minfuncreal(A)).(g,h))
 proof
    now let x be Element of A;
 A1: x in dom (minreal.:(f,g)) by Lm10;
 A2: x in dom (minreal.:(g,h)) by Lm10;
 A3: x in dom (minreal.:(f,(minreal.:(g,h)))) by Lm10;
 A4: x in dom (minreal.:((minreal.:(f,g)),h)) by Lm10;
 thus ((minfuncreal(A)).((minfuncreal(A)).(f,g),h)).x
           =((minfuncreal(A)).(minreal.:(f,g),h)).x by Def6
          .=(minreal.:(minreal.:(f,g),h)).x by Def6
          .=minreal.((minreal.:(f,g)).x,h.x) by A4,FUNCOP_1:28
          .=minreal.(minreal.(f.x,g.x),h.x) by A1,FUNCOP_1:28
          .=minreal.(f.x,minreal.(g.x,h.x)) by Def4,Th11
          .=minreal.(f.x,((minreal.:(g,h)).x)) by A2,FUNCOP_1:28
          .=(minreal.:(f,(minreal.:(g,h)))).x by A3,FUNCOP_1:28
          .=((minfuncreal(A)).(f,(minreal.:(g,h)))).x by Def6
          .=((minfuncreal(A)).(f,((minfuncreal(A)).(g,h)))).x by Def6;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem Th24:
 (maxfuncreal(A)).(f,(minfuncreal(A)).(f,g))=f
proof
    now let x be Element of A;
 A1: x in dom (minreal.:(f,g)) by Lm10;
 A2: x in dom (maxreal.:(f,(minreal.:(f,g)))) by Lm10;
 thus (maxfuncreal(A)).(f,(minfuncreal(A)).(f,g)).x
           =((maxfuncreal(A)).(f,minreal.:(f,g))).x by Def6
          .=(maxreal.:(f,minreal.:(f,g))).x by Def5
          .=maxreal.(f.x,(minreal.:(f,g)).x) by A2,FUNCOP_1:28
          .=maxreal.(f.x,(minreal.(f.x,g.x))) by A1,FUNCOP_1:28
          .=f.x by Def4,Th12;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem Th25:
 (maxfuncreal(A)).((minfuncreal(A)).(f,g),f)=f
proof
  thus (maxfuncreal(A)).((minfuncreal(A)).(f,g),f)
           =(maxfuncreal(A)).(f,(minfuncreal(A)).(f,g)) by Th20
          .=f by Th24;
end;

theorem Th26:
 (maxfuncreal(A)).((minfuncreal(A)).(g,f),f)=f
proof
  thus (maxfuncreal(A)).((minfuncreal(A)).(g,f),f)
           =(maxfuncreal(A)).((minfuncreal(A)).(f,g),f) by Th21
          .=f by Th25;
end;

theorem
   (maxfuncreal(A)).(f,(minfuncreal(A)).(g,f))=f
proof
  thus (maxfuncreal(A)).(f,(minfuncreal(A)).(g,f))
           =(maxfuncreal(A)).(f,(minfuncreal(A)).(f,g)) by Th21
          .=f by Th24;
end;

theorem Th28:
 (minfuncreal(A)).(f,(maxfuncreal(A)).(f,g))=f
proof
    now let x be Element of A;
 A1: x in dom (maxreal.:(f,g)) by Lm10;
 A2: x in dom (minreal.:(f,(maxreal.:(f,g)))) by Lm10;
 thus (minfuncreal(A)).(f,(maxfuncreal(A)).(f,g)).x
           =((minfuncreal(A)).(f,maxreal.:(f,g))).x by Def5
          .=(minreal.:(f,maxreal.:(f,g))).x by Def6
          .=minreal.(f.x,(maxreal.:(f,g)).x) by A2,FUNCOP_1:28
          .=minreal.(f.x,(maxreal.(f.x,g.x))) by A1,FUNCOP_1:28
          .=f.x by Def4,Th13;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem Th29:
 (minfuncreal(A)).(f,(maxfuncreal(A)).(g,f))=f
proof
 thus (minfuncreal(A)).(f,(maxfuncreal(A)).(g,f))
          =(minfuncreal(A)).(f,(maxfuncreal(A)).(f,g)) by Th20
         .=f by Th28;
end;

theorem Th30:
 (minfuncreal(A)).((maxfuncreal(A)).(g,f),f)=f
proof
 thus (minfuncreal(A)).((maxfuncreal(A)).(g,f),f)
          =(minfuncreal(A)).(f,(maxfuncreal(A)).(g,f)) by Th21
         .=f by Th29;
end;

theorem
   (minfuncreal(A)).((maxfuncreal(A)).(f,g),f)=f
proof
 thus (minfuncreal(A)).((maxfuncreal(A)).(f,g),f)
          =(minfuncreal(A)).((maxfuncreal(A)).(g,f),f) by Th20
         .=f by Th30;
end;

theorem Th32:
 (minfuncreal(A)).(f,(maxfuncreal(A)).(g,h)) =
 (maxfuncreal(A)).((minfuncreal(A)).(f,g),(minfuncreal(A)).(f,h))
proof
    now let x be Element of A;
 A1: x in dom (minreal.:(f,g)) by Lm10;
 A2: x in dom (minreal.:(f,h)) by Lm10;
 A3: x in dom (maxreal.:(g,h)) by Lm10;
 A4: x in dom (maxreal.:(minreal.:(f,g),minreal.:(f,h))) by Lm10;
 A5: x in dom (minreal.:(f,(maxreal.:(g,h)))) by Lm10;
 thus (minfuncreal(A)).(f,(maxfuncreal(A)).(g,h)).x
     =((minfuncreal(A)).(f,maxreal.:(g,h))).x by Def5
    .=(minreal.:(f,maxreal.:(g,h))).x by Def6
    .=minreal.(f.x,(maxreal.:(g,h)).x) by A5,FUNCOP_1:28
    .=minreal.(f.x,(maxreal.(g.x,h.x))) by A3,FUNCOP_1:28
    .=maxreal.(minreal.(f.x,g.x),minreal.(f.x,h.x)) by Def4,Th14
    .=maxreal.(minreal.:(f,g).x,minreal.(f.x,h.x)) by A1,FUNCOP_1:28
    .=maxreal.(minreal.:(f,g).x,minreal.:(f,h).x) by A2,FUNCOP_1:28
    .=maxreal.:(minreal.:(f,g),minreal.:(f,h)).x by A4,FUNCOP_1:28
    .=(maxfuncreal(A)).(minreal.:(f,g),minreal.:(f,h)).x by Def5
    .=(maxfuncreal(A)).((minfuncreal(A)).(f,g),minreal.:(f,h)).x by Def6
    .=(maxfuncreal(A)).((minfuncreal(A)).(f,g),(minfuncreal(A)).(f,h)).x
    by Def6;
   end;
  hence thesis by FUNCT_2:113;
 end;

 reserve p,q,r for Element of
        LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);

definition let A;
 let x be Element of
  LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
 canceled 2;

 func @x->Element of Funcs(A,REAL) equals
    x;
 coherence;
end;

Lm11:
 for a,b being Element of
  LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #)
       holds a"\/"b = b"\/"a
 proof
  let a,b be Element of
  LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
  thus a"\/"b = (maxfuncreal(A)).(a,b) by LATTICES:def 1
           .= (maxfuncreal(A)).(b,a) by Th20
           .= b"\/"a by LATTICES:def 1;
 end;

Lm12:
 for a,b being Element of
  LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #)
       holds a"/\"b = b"/\"a
 proof
  let a,b be Element of
   LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
  thus a"/\"b = (minfuncreal(A)).(a,b) by LATTICES:def 2
           .= (minfuncreal(A)).(b,a) by Th21
           .= b"/\"a by LATTICES:def 2;
 end;

Lm13:
for a,b,c being Element of
 LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #)
      holds a"\/"(b"\/"c) = (a"\/"b)"\/"c
 proof
  let a,b,c be Element of
  LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
  thus a"\/"(b"\/"c) = (maxfuncreal(A)).(a,b"\/"c) by LATTICES:def 1
                .= (maxfuncreal(A)).(a,(maxfuncreal(A)).(b,c)) by LATTICES:def
1
                .= (maxfuncreal(A)).((maxfuncreal(A)).(a,b),c) by Th22
                .= (maxfuncreal(A)).(a"\/"b,c) by LATTICES:def 1
                .= (a"\/"b)"\/"c by LATTICES:def 1;
end;

Lm14:
for a,b,c being Element of
LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #)
      holds a"/\"(b"/\"c) = (a"/\"b)"/\"c
 proof
  let a,b,c be Element of
  LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
  thus a"/\"(b"/\"c) = (minfuncreal(A)).(a,b"/\"c) by LATTICES:def 2
                .= (minfuncreal(A)).(a,(minfuncreal(A)).(b,c)) by LATTICES:def
2
                .= (minfuncreal(A)).((minfuncreal(A)).(a,b),c) by Th23
                .= (minfuncreal(A)).(a"/\"b,c) by LATTICES:def 2
                .= (a"/\"b)"/\"c by LATTICES:def 2;
end;

Lm15:
for a,b,c being Element of
LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #)
      holds (a"/\"b)"\/"b = b
 proof
  let a,b,c be Element of
  LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
  thus (a"/\"b)"\/"b = (maxfuncreal(A)).(a"/\"b,b) by LATTICES:def 1
                .= (maxfuncreal(A)).((minfuncreal(A)).(a,b),b) by LATTICES:def
2
                .= b by Th26;
end;

Lm16:
for a,b,c being Element of
LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #)
      holds a"/\"(a"\/"b) = a
 proof
  let a,b,c be Element of
  LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
  thus a"/\"(a"\/"b) = (minfuncreal(A)).(a,a"\/"b) by LATTICES:def 2
                .= (minfuncreal(A)).(a,(maxfuncreal(A)).(a,b)) by LATTICES:def
1
                .= a by Th28;
end;

definition let A;
 func RealFunc_Lattice(A) -> strict Lattice equals
 :Def10: LattStr (# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
 coherence
  proof
     LattStr (# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) is
Lattice-like
     proof
      thus (for p,q holds p"\/"q = q"\/"p) &
      (for p,q,r holds p"\/"(q"\/"r) = (p"\/"q)"\/"r) &
      (for p,q holds (p"/\"q)"\/"q = q) &
      (for p,q holds p"/\"q = q"/\"p) &
      (for p,q,r holds p"/\"(q"/\"r) = (p"/\"q)"/\"r) &
      (for p,q holds p"/\"(p"\/"q) = p) by Lm11,Lm12,Lm13,Lm14,Lm15,Lm16;
     end;
   hence thesis;
  end;
end;

Lm17:
for a,b,c being Element of RealFunc_Lattice(A)
 holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c)
 proof
  let a',b',c' be Element of RealFunc_Lattice(A);
  A1:RealFunc_Lattice(A)=
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
  reconsider a=a',b=b',c =c' as Element of
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
  set l=a"/\"c;
  thus a'"/\"(b'"\/"c') = (minfuncreal(A)).(a,b"\/"c) by A1,LATTICES:def 2
    .= (minfuncreal(A)).(a,(maxfuncreal(A)).(b,c)) by LATTICES:def 1
    .=(maxfuncreal(A)).((minfuncreal(A)).(a,b),(minfuncreal(A)).(a,c))
    by Th32
    .= (maxfuncreal(A)).((minfuncreal(A)).(a,b),l) by LATTICES:def 2
    .= (maxfuncreal(A)).(a"/\"b,l) by LATTICES:def 2
    .= (a'"/\"b')"\/"(a'"/\"c') by A1,LATTICES:def 1;
 end;

reserve p,q,r for Element of RealFunc_Lattice(A);

canceled 7;

theorem Th40:
(maxfuncreal(A)).(p,q) = (maxfuncreal(A)).(q,p)
 proof
 A1:RealFunc_Lattice(A)=
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
 hence (maxfuncreal(A)).(p,q) = q"\/"p by LATTICES:def 1
                   .= (maxfuncreal(A)).(q,p) by A1,LATTICES:def 1;
 end;

theorem Th41:
(minfuncreal(A)).(p,q) = (minfuncreal(A)).(q,p)
 proof
 A1:RealFunc_Lattice(A)=
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
 hence (minfuncreal(A)).(p,q) = q"/\"p by LATTICES:def 2
                   .= (minfuncreal(A)).(q,p) by A1,LATTICES:def 2;
 end;

theorem
   (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
              =(maxfuncreal(A)).(((maxfuncreal(A)).(q,r)),p) &
 (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
              =(maxfuncreal(A)).(((maxfuncreal(A)).(p,q)),r) &
 (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
              =(maxfuncreal(A)).(((maxfuncreal(A)).(q,p)),r) &
 (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
              =(maxfuncreal(A)).(((maxfuncreal(A)).(r,p)),q) &
 (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
              =(maxfuncreal(A)).(((maxfuncreal(A)).(r,q)),p) &
 (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
              =(maxfuncreal(A)).(((maxfuncreal(A)).(p,r)),q)
 proof
 set s=q"\/"r;
 A1:RealFunc_Lattice(A)=
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
 hence A2:(maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
                    =(maxfuncreal(A)).(p,s) by LATTICES:def 1
                   .= s"\/"p by A1,LATTICES:def 1
                   .= (maxfuncreal(A)).(s,p) by A1,LATTICES:def 1
                   .= (maxfuncreal(A)).(((maxfuncreal(A)).(q,r)),p) by A1,
LATTICES:def 1;
 thus (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
                    =(maxfuncreal(A)).(p,s) by A1,LATTICES:def 1
                   .= p"\/"s by A1,LATTICES:def 1
                   .= (p"\/"q)"\/"r by A1,Lm13
                   .= (maxfuncreal(A)).(p"\/"q,r) by A1,LATTICES:def 1
                   .= (maxfuncreal(A)).((maxfuncreal(A)).(p,q),r) by A1,
LATTICES:def 1;
 thus (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
                    =(maxfuncreal(A)).(p,s) by A1,LATTICES:def 1
                   .= p"\/"s by A1,LATTICES:def 1
                   .= (q"\/"p)"\/"r by A1,Lm13
                   .= (maxfuncreal(A)).(q"\/"p,r) by A1,LATTICES:def 1
                   .= (maxfuncreal(A)).((maxfuncreal(A)).(q,p),r) by A1,
LATTICES:def 1;
 thus A3:(maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
                    =(maxfuncreal(A)).(p,s) by A1,LATTICES:def 1
                   .= p"\/"(r"\/"q) by A1,LATTICES:def 1
                   .= (r"\/"p)"\/"q by A1,Lm13
                   .= (maxfuncreal(A)).(r"\/"p,q) by A1,LATTICES:def 1
                   .= (maxfuncreal(A)).((maxfuncreal(A)).(r,p),q) by A1,
LATTICES:def 1;
 thus (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))=
        (maxfuncreal(A)).(((maxfuncreal(A)).(r,q)),p) by A2,Th40;
 thus (maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))=
        (maxfuncreal(A)).(((maxfuncreal(A)).(p,r)),q) by A3,Th40;
end;

theorem
   (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
            =(minfuncreal(A)).(((minfuncreal(A)).(q,r)),p) &
 (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
            =(minfuncreal(A)).(((minfuncreal(A)).(p,q)),r) &
 (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
            =(minfuncreal(A)).(((minfuncreal(A)).(q,p)),r) &
 (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
            =(minfuncreal(A)).(((minfuncreal(A)).(r,p)),q) &
 (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
            =(minfuncreal(A)).(((minfuncreal(A)).(r,q)),p) &
 (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
            =(minfuncreal(A)).(((minfuncreal(A)).(p,r)),q)
 proof
 set s=q"/\"r;
 A1:RealFunc_Lattice(A)=
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
 hence A2:(minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
                    =(minfuncreal(A)).(p,s) by LATTICES:def 2
                   .= s"/\"p by A1,LATTICES:def 2
                   .= (minfuncreal(A)).(s,p) by A1,LATTICES:def 2
                   .= (minfuncreal(A)).(((minfuncreal(A)).(q,r)),p) by A1,
LATTICES:def 2;
 thus (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
                    =(minfuncreal(A)).(p,s) by A1,LATTICES:def 2
                   .= p"/\"s by A1,LATTICES:def 2
                   .= (p"/\"q)"/\"r by A1,Lm14
                   .= (minfuncreal(A)).(p"/\"q,r) by A1,LATTICES:def 2
                   .= (minfuncreal(A)).((minfuncreal(A)).(p,q),r) by A1,
LATTICES:def 2;
 thus (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
                    =(minfuncreal(A)).(p,s) by A1,LATTICES:def 2
                   .= p"/\"s by A1,LATTICES:def 2
                   .= (q"/\"p)"/\"r by A1,Lm14
                   .= (minfuncreal(A)).(q"/\"p,r) by A1,LATTICES:def 2
                   .= (minfuncreal(A)).((minfuncreal(A)).(q,p),r) by A1,
LATTICES:def 2;
 thus A3:(minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
                    =(minfuncreal(A)).(p,s) by A1,LATTICES:def 2
                   .= p"/\"(r"/\"q) by A1,LATTICES:def 2
                   .= (r"/\"p)"/\"q by A1,Lm14
                   .= (minfuncreal(A)).(r"/\"p,q) by A1,LATTICES:def 2
                   .= (minfuncreal(A)).((minfuncreal(A)).(r,p),q) by A1,
LATTICES:def 2;
 thus (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
         =(minfuncreal(A)).(((minfuncreal(A)).(r,q)),p) by A2,Th41;
 thus (minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
         =(minfuncreal(A)).(((minfuncreal(A)).(p,r)),q) by A3,Th41;
end;

theorem
   (maxfuncreal(A)).((minfuncreal(A)).(p,q),q)=q &
 (maxfuncreal(A)).(q,(minfuncreal(A)).(p,q))=q &
 (maxfuncreal(A)).(q,(minfuncreal(A)).(q,p))=q &
 (maxfuncreal(A)).((minfuncreal(A)).(q,p),q)=q
 proof
 set s=p"/\"q;
 A1:RealFunc_Lattice(A)=
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
 hence A2:(maxfuncreal(A)).((minfuncreal(A)).(p,q),q)
                   =(maxfuncreal(A)).(s,q) by LATTICES:def 2
                              .=s"\/"q by A1,LATTICES:def 1
                              .=q by A1,Lm15;
 thus (maxfuncreal(A)).(q,(minfuncreal(A)).(p,q))
                   =(maxfuncreal(A)).(q,s) by A1,LATTICES:def 2
                              .=(p"/\"q)"\/"q by A1,LATTICES:def 1
                              .=q by A1,Lm15;
 thus (maxfuncreal(A)).(q,(minfuncreal(A)).(q,p))
                  =(maxfuncreal(A)).(q,q"/\"p) by A1,LATTICES:def 2
                              .=(p"/\"q)"\/"q by A1,LATTICES:def 1
                              .=q by A1,Lm15;
 thus (maxfuncreal(A)).((minfuncreal(A)).(q,p),q)=q by A2,Th41;
 end;

theorem
   (minfuncreal(A)).(q,(maxfuncreal(A)).(q,p))=q &
 (minfuncreal(A)).((maxfuncreal(A)).(p,q),q)=q &
 (minfuncreal(A)).(q,(maxfuncreal(A)).(p,q))=q &
 (minfuncreal(A)).((maxfuncreal(A)).(q,p),q)=q
 proof
 set s=q"\/"p;
 A1:RealFunc_Lattice(A)=
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
 hence A2:(minfuncreal(A)).(q,(maxfuncreal(A)).(q,p))
                    =(minfuncreal(A)).(q,s) by LATTICES:def 1
                              .=q"/\"s by A1,LATTICES:def 2
                              .=q by A1,Lm16;
 thus A3:(minfuncreal(A)).((maxfuncreal(A)).(p,q),q)
                      =(minfuncreal(A)).(p"\/"q,q) by A1,LATTICES:def 1
                              .=q"/\"(q"\/"p) by A1,LATTICES:def 2
                              .=q by A1,Lm16;
 thus (minfuncreal(A)).(q,(maxfuncreal(A)).(p,q))=q by A2,Th40;
 thus (minfuncreal(A)).((maxfuncreal(A)).(q,p),q)=q by A3,Th40;
end;

theorem
   (minfuncreal(A)).(q,(maxfuncreal(A)).(p,r))
      =(maxfuncreal(A)).((minfuncreal(A)).(q,p),(minfuncreal(A)).(q,r))
 proof
 set s=p"\/"r;
 A1:RealFunc_Lattice(A)=
  LattStr (#Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #) by Def10;
 set w=q"/\"r;
 thus (minfuncreal(A)).(q,(maxfuncreal(A)).(p,r))
                  =(minfuncreal(A)).(q,s) by A1,LATTICES:def 1
                 .=q"/\"s by A1,LATTICES:def 2
                 .=(q"/\"p)"\/"(q"/\"r) by Lm17
                 .=(maxfuncreal(A)).(q"/\"p,w) by A1,LATTICES:def 1
                 .=(maxfuncreal(A)).((minfuncreal(A)).(q,p),w) by A1,LATTICES:
def 2
 .=(maxfuncreal(A)).((minfuncreal(A)).(q,p),(minfuncreal(A)).(q,r)) by A1,
LATTICES:def 2;
end;

theorem
   RealFunc_Lattice(A) is D_Lattice
 proof
     p"/\"(q"\/"r) = (p"/\"q)"\/"(p"/\"r) by Lm17;
  hence RealFunc_Lattice(A) is D_Lattice by LATTICES:def 11;
 end;

Back to top