lattice2.miz

    begin

    reserve A for set,

C for non empty set,

B for Subset of A,

x for Element of A,

f,g for Function of A, C;

    theorem :: LATTICE2:1



     Th1: ( dom (g | B)) = B

    proof



      thus ( dom (g | B)) = (( dom g) /\ B) by RELAT_1: 61

      .= (A /\ B) by FUNCT_2:def 1

      .= B by XBOOLE_1: 28;

    end;

    theorem :: LATTICE2:2



     Th2: (f | B) = (g | B) iff for x st x in B holds (g . x) = (f . x)

    proof

      thus (f | B) = (g | B) implies for x st x in B holds (g . x) = (f . x)

      proof

        assume

         A1: (f | B) = (g | B);

        let x;

        assume

         A2: x in B;



        hence (g . x) = ((g | B) . x) by FUNCT_1: 49

        .= (f . x) by A1, A2, FUNCT_1: 49;

      end;

      reconsider f9 = (f | B), g9 = (g | B) as Function of B, C by FUNCT_2: 32;

      assume

       A3: for x st x in B holds (g . x) = (f . x);

       A4:

      now

        let x be object;

        assume

         A5: x in B;



        hence (f9 . x) = (f . x) by FUNCT_1: 49

        .= (g . x) by A3, A5

        .= (g9 . x) by A5, FUNCT_1: 49;

      end;



      thus (f | B) = (f9 | B)

      .= (g9 | B) by A4, FUNCT_2: 12

      .= (g | B);

    end;

    theorem :: LATTICE2:3



     Th3: for B be set holds (f +* (g | B)) is Function of A, C

    proof

      let B be set;



       A1: ( dom f) = A & ( dom g) = A by FUNCT_2:def 1;

      ( dom (f +* (g | B))) = (( dom f) \/ ( dom (g | B))) by FUNCT_4:def 1

      .= (( dom f) \/ (( dom g) /\ B)) by RELAT_1: 61

      .= A by A1, XBOOLE_1: 22;

      hence thesis by FUNCT_2: 67;

    end;

    theorem :: LATTICE2:4



     Th4: ((g | B) +* f) = f

    proof

      ( dom (g | B)) = B & ( dom f) = A by Th1, FUNCT_2:def 1;

      hence thesis by FUNCT_4: 19;

    end;

    theorem :: LATTICE2:5



     Th5: for f,g be Function holds g c= f implies (f +* g) = f

    proof

      let f,g be Function;

      assume

       A1: g c= f;

      then ( dom g) c= ( dom f) by GRFUNC_1: 2;

      then

       A2: ( dom f) = (( dom f) \/ ( dom g)) by XBOOLE_1: 12;

      for x be object st x in ( dom f) holds (x in ( dom g) implies (f . x) = (g . x)) & ( not x in ( dom g) implies (f . x) = (f . x)) by A1, GRFUNC_1: 2;

      hence thesis by A2, FUNCT_4:def 1;

    end;

    theorem :: LATTICE2:6

    (f +* (f | B)) = f by Th5, RELAT_1: 59;

    theorem :: LATTICE2:7



     Th7: (for x st x in B holds (g . x) = (f . x)) implies (f +* (g | B)) = f

    proof

      assume x in B implies (g . x) = (f . x);

      then (g | B) = (f | B) by Th2;

      hence thesis by Th5, RELAT_1: 59;

    end;

    reserve B for Element of ( Fin A);

    theorem :: LATTICE2:8

    ((g | B) +* f) = f

    proof

      reconsider C = B as Subset of A by FINSUB_1: 16;

      ((g | C) +* f) = f by Th4;

      hence thesis;

    end;

    theorem :: LATTICE2:9



     Th9: ( dom (g | B)) = B

    proof

      reconsider C = B as Subset of A by FINSUB_1: 16;

      ( dom (g | C)) = C by Th1;

      hence thesis;

    end;

    theorem :: LATTICE2:10



     Th10: (for x st x in B holds (g . x) = (f . x)) implies (f +* (g | B)) = f

    proof

      reconsider C = B as Subset of A by FINSUB_1: 16;

      (for x st x in C holds (g . x) = (f . x)) implies (f +* (g | C)) = f by Th7;

      hence thesis;

    end;

    definition

      let D be non empty set;

      let o,o9 be BinOp of D;

      :: LATTICE2:def1

      pred o absorbs o9 means for x,y be Element of D holds (o . (x,(o9 . (x,y)))) = x;

    end

    notation

      let D be non empty set;

      let o,o9 be BinOp of D;

      antonym o doesn't_absorb o9 for o absorbs o9;

    end

    reserve L for non empty LattStr,

a,b,c for Element of L;

    theorem :: LATTICE2:11



     Th11: the L_join of L is commutative associative & the L_meet of L is commutative associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L implies L is Lattice-like

    proof

      assume that

       A1: the L_join of L is commutative and

       A2: the L_join of L is associative and

       A3: the L_meet of L is commutative and

       A4: the L_meet of L is associative and

       A5: the L_join of L absorbs the L_meet of L and

       A6: the L_meet of L absorbs the L_join of L;

      thus (a "\/" b) = (b "\/" a) by A1;

      thus (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c) by A2;

      thus ((a "/\" b) "\/" b) = b

      proof



        thus ((a "/\" b) "\/" b) = (b "\/" (a "/\" b)) by A1

        .= (b "\/" (b "/\" a)) by A3

        .= b by A5;

      end;

      thus (a "/\" b) = (b "/\" a) by A3;

      thus (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c) by A4;

      let a, b;

      thus thesis by A6;

    end;

    definition

      let L be LattStr;

      :: LATTICE2:def2

      func L .: -> strict LattStr equals LattStr (# the carrier of L, the L_meet of L, the L_join of L #);

      correctness ;

    end

    registration

      let L be non empty LattStr;

      cluster (L .: ) -> non empty;

      coherence ;

    end

    theorem :: LATTICE2:12

    the carrier of L = the carrier of (L .: ) & the L_join of L = the L_meet of (L .: ) & the L_meet of L = the L_join of (L .: );

    theorem :: LATTICE2:13

    for L be strict non empty LattStr holds ((L .: ) .: ) = L;

    reserve L for Lattice;

    reserve a,b,c,u,v for Element of L;

    theorem :: LATTICE2:14



     Th14: (for v holds (u "\/" v) = v) implies u = ( Bottom L)

    proof

      assume

       A1: (u "\/" v) = v;

      now

        let v;

        (v "\/" u) = v by A1;

        then u [= v;

        hence (v "/\" u) = u by LATTICES: 4;

      end;

      hence thesis by RLSUB_2: 64;

    end;

    theorem :: LATTICE2:15



     Th15: (for v holds (the L_join of L . (u,v)) = v) implies u = ( Bottom L)

    proof

      assume for v holds (the L_join of L . (u,v)) = v;

      then for v holds (u "\/" v) = v;

      hence thesis by Th14;

    end;

    theorem :: LATTICE2:16



     Th16: (for v holds (u "/\" v) = v) implies u = ( Top L)

    proof

      assume

       A1: (u "/\" v) = v;

      now

        let v;

        (v "/\" u) = v by A1;

        then v [= u by LATTICES: 4;

        hence u = (v "\/" u);

      end;

      hence thesis by RLSUB_2: 65;

    end;

    theorem :: LATTICE2:17



     Th17: (for v holds (the L_meet of L . (u,v)) = v) implies u = ( Top L)

    proof

      assume for v holds (the L_meet of L . (u,v)) = v;

      then for v holds (u "/\" v) = v;

      hence thesis by Th16;

    end;

    registration

      let L;

      cluster the L_join of L -> idempotent;

      coherence

      proof

        let a;



        thus (the L_join of L . (a,a)) = (a "\/" a)

        .= a;

      end;

    end

    registration

      let L be join-commutative non empty \/-SemiLattStr;

      cluster the L_join of L -> commutative;

      coherence

      proof

        let a,b be Element of L;



        thus (the L_join of L . (a,b)) = (b "\/" a) by LATTICES:def 1

        .= (the L_join of L . (b,a));

      end;

    end

    theorem :: LATTICE2:18



     Th18: the L_join of L is having_a_unity implies ( Bottom L) = ( the_unity_wrt the L_join of L)

    proof

      set J = the L_join of L;

      given u such that

       A1: u is_a_unity_wrt J;

      (the L_join of L . (u,v)) = v by A1, BINOP_1: 4;

      then u = ( Bottom L) by Th15;

      hence thesis by A1, BINOP_1:def 8;

    end;

    registration

      let L be join-associative non empty \/-SemiLattStr;

      cluster the L_join of L -> associative;

      coherence

      proof

        let a,b,c be Element of L;



        thus (the L_join of L . (a,(the L_join of L . (b,c)))) = (a "\/" (b "\/" c))

        .= ((a "\/" b) "\/" c) by LATTICES:def 5

        .= (the L_join of L . ((the L_join of L . (a,b)),c));

      end;

    end

    registration

      let L;

      cluster the L_meet of L -> idempotent;

      coherence

      proof

        let a;



        thus (the L_meet of L . (a,a)) = (a "/\" a)

        .= a;

      end;

    end

    registration

      let L be meet-commutative non empty /\-SemiLattStr;

      cluster the L_meet of L -> commutative;

      coherence

      proof

        let a,b be Element of L;



        thus (the L_meet of L . (a,b)) = (b "/\" a) by LATTICES:def 2

        .= (the L_meet of L . (b,a));

      end;

    end

    registration

      let L be meet-associative non empty /\-SemiLattStr;

      cluster the L_meet of L -> associative;

      coherence

      proof

        let a,b,c be Element of L;



        thus (the L_meet of L . (a,(the L_meet of L . (b,c)))) = (a "/\" (b "/\" c))

        .= ((a "/\" b) "/\" c) by LATTICES:def 7

        .= (the L_meet of L . ((the L_meet of L . (a,b)),c));

      end;

    end

    theorem :: LATTICE2:19



     Th19: the L_meet of L is having_a_unity implies ( Top L) = ( the_unity_wrt the L_meet of L)

    proof

      set J = the L_meet of L;

      given u such that

       A1: u is_a_unity_wrt J;

      (the L_meet of L . (u,v)) = v by A1, BINOP_1: 4;

      then u = ( Top L) by Th17;

      hence thesis by A1, BINOP_1:def 8;

    end;

    theorem :: LATTICE2:20



     Th20: the L_join of L is_distributive_wrt the L_join of L

    proof

      now

        let a, b, c;



        thus (the L_join of L . (a,(the L_join of L . (b,c)))) = (a "\/" (b "\/" c))

        .= ((a "\/" b) "\/" c) by LATTICES:def 5

        .= (((a "\/" a) "\/" b) "\/" c)

        .= (((a "\/" b) "\/" a) "\/" c) by LATTICES:def 5

        .= ((a "\/" b) "\/" (a "\/" c)) by LATTICES:def 5

        .= (the L_join of L . ((the L_join of L . (a,b)),(the L_join of L . (a,c))));

      end;

      hence thesis by BINOP_1: 12;

    end;

    theorem :: LATTICE2:21

    L is D_Lattice implies the L_join of L is_distributive_wrt the L_meet of L

    proof

      assume

       A1: L is D_Lattice;

      now

        let a, b, c;



        thus (the L_join of L . (a,(the L_meet of L . (b,c)))) = (a "\/" (b "/\" c))

        .= ((a "\/" b) "/\" (a "\/" c)) by A1, LATTICES: 11

        .= (the L_meet of L . ((the L_join of L . (a,b)),(the L_join of L . (a,c))));

      end;

      hence thesis by BINOP_1: 12;

    end;

    theorem :: LATTICE2:22



     Th22: the L_join of L is_distributive_wrt the L_meet of L implies L is distributive

    proof

      assume

       A1: the L_join of L is_distributive_wrt the L_meet of L;

      then

       A2: for a, b, c holds (a "\/" (b "/\" c)) = ((a "\/" b) "/\" (a "\/" c)) by BINOP_1: 12;

      let a, b, c;



      thus (a "/\" (b "\/" c)) = ((a "/\" (c "\/" a)) "/\" (c "\/" b)) by LATTICES:def 9

      .= (a "/\" ((c "\/" a) "/\" (c "\/" b))) by LATTICES:def 7

      .= (a "/\" ((a "/\" b) "\/" c)) by A2

      .= (((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" c)) by LATTICES:def 8

      .= ((a "/\" b) "\/" (a "/\" c)) by A1, BINOP_1: 12;

    end;

    theorem :: LATTICE2:23



     Th23: L is D_Lattice implies the L_meet of L is_distributive_wrt the L_join of L

    proof

      assume

       A1: L is D_Lattice;

      now

        let a, b, c;



        thus (the L_meet of L . (a,(the L_join of L . (b,c)))) = (a "/\" (b "\/" c))

        .= ((a "/\" b) "\/" (a "/\" c)) by A1, LATTICES:def 11

        .= (the L_join of L . ((the L_meet of L . (a,b)),(the L_meet of L . (a,c))));

      end;

      hence thesis by BINOP_1: 12;

    end;

    theorem :: LATTICE2:24

    the L_meet of L is_distributive_wrt the L_join of L implies L is distributive by BINOP_1: 12;

    theorem :: LATTICE2:25



     Th25: the L_meet of L is_distributive_wrt the L_meet of L

    proof

      now

        let a, b, c;



        thus (the L_meet of L . (a,(the L_meet of L . (b,c)))) = (a "/\" (b "/\" c))

        .= ((a "/\" b) "/\" c) by LATTICES:def 7

        .= (((a "/\" a) "/\" b) "/\" c)

        .= (((a "/\" b) "/\" a) "/\" c) by LATTICES:def 7

        .= ((a "/\" b) "/\" (a "/\" c)) by LATTICES:def 7

        .= (the L_meet of L . ((the L_meet of L . (a,b)),(the L_meet of L . (a,c))));

      end;

      hence thesis by BINOP_1: 12;

    end;

    theorem :: LATTICE2:26



     Th26: the L_join of L absorbs the L_meet of L

    proof

      let x,y be Element of L;



      thus (the L_join of L . (x,(the L_meet of L . (x,y)))) = (x "\/" (x "/\" y))

      .= x by LATTICES:def 8;

    end;

    theorem :: LATTICE2:27



     Th27: the L_meet of L absorbs the L_join of L

    proof

      let x,y be Element of L;



      thus (the L_meet of L . (x,(the L_join of L . (x,y)))) = (x "/\" (x "\/" y))

      .= x by LATTICES:def 9;

    end;

    definition

      let A be non empty set, L be Lattice;

      let B be Element of ( Fin A);

      let f be Function of A, the carrier of L;

      :: LATTICE2:def3

      func FinJoin (B,f) -> Element of L equals (the L_join of L $$ (B,f));

      correctness ;

      :: LATTICE2:def4

      func FinMeet (B,f) -> Element of L equals (the L_meet of L $$ (B,f));

      correctness ;

    end

    reserve A for non empty set,

x for Element of A,

B for Element of ( Fin A),

f,g for Function of A, the carrier of L;

    theorem :: LATTICE2:28



     Th28: x in B implies (f . x) [= ( FinJoin (B,f)) by SETWISEO: 22;

    theorem :: LATTICE2:29



     Th29: (ex x st x in B & u [= (f . x)) implies u [= ( FinJoin (B,f))

    proof

      given x such that

       A1: x in B and

       A2: u [= (f . x);

      (f . x) [= ( FinJoin (B,f)) by A1, Th28;

      then

       A3: ((f . x) "\/" ( FinJoin (B,f))) = ( FinJoin (B,f));



      then (u "\/" ( FinJoin (B,f))) = ((u "\/" (f . x)) "\/" ( FinJoin (B,f))) by LATTICES:def 5

      .= ( FinJoin (B,f)) by A2, A3;

      hence thesis;

    end;

    theorem :: LATTICE2:30

    (for x st x in B holds (f . x) = u) & B <> {} implies ( FinJoin (B,f)) = u by SETWISEO: 24;

    theorem :: LATTICE2:31

    ( FinJoin (B,f)) [= u implies for x st x in B holds (f . x) [= u

    proof

      assume

       A1: ( FinJoin (B,f)) [= u;

      let x;

      assume x in B;

      then (f . x) [= ( FinJoin (B,f)) by Th28;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: LATTICE2:32



     Th32: B <> {} & (for x st x in B holds (f . x) [= u) implies ( FinJoin (B,f)) [= u

    proof

      assume that

       A1: B <> {} and

       A2: for x st x in B holds (f . x) [= u;

      set J = the L_join of L;

       A3:

      now

        let x;

        assume x in B;

        then

         A4: (f . x) [= u by A2;



        thus ((J [:] (f,u)) . x) = ((f . x) "\/" u) by FUNCOP_1: 48

        .= u by A4;

      end;

      (( FinJoin (B,f)) "\/" u) = (J $$ (B,(J [:] (f,u)))) by A1, Th20, SETWISEO: 28

      .= u by A1, A3, SETWISEO: 24;

      hence thesis;

    end;

    theorem :: LATTICE2:33

    B <> {} & (for x st x in B holds (f . x) [= (g . x)) implies ( FinJoin (B,f)) [= ( FinJoin (B,g))

    proof

      assume that

       A1: B <> {} and

       A2: for x st x in B holds (f . x) [= (g . x);

      now

        let x;

        assume

         A3: x in B;

        then (f . x) [= (g . x) by A2;

        hence (f . x) [= ( FinJoin (B,g)) by A3, Th29;

      end;

      hence thesis by A1, Th32;

    end;

    theorem :: LATTICE2:34



     Th34: B <> {} & (f | B) = (g | B) implies ( FinJoin (B,f)) = ( FinJoin (B,g))

    proof

      assume that

       A1: B <> {} and

       A2: (f | B) = (g | B);

      (f .: B) = (g .: B) by A2, RELAT_1: 166;

      hence thesis by A1, SETWISEO: 26;

    end;

    theorem :: LATTICE2:35

    B <> {} implies (v "\/" ( FinJoin (B,f))) = ( FinJoin (B,(the L_join of L [;] (v,f)))) by Th20, SETWISEO: 27;

    registration

      let L be Lattice;

      cluster (L .: ) -> Lattice-like;

      coherence

      proof

        the L_join of (L .: ) absorbs the L_meet of (L .: ) & the L_meet of (L .: ) absorbs the L_join of (L .: ) by Th26, Th27;

        hence thesis by Th11;

      end;

    end

    theorem :: LATTICE2:36

    for L be Lattice, B be Element of ( Fin A) holds for f be Function of A, the carrier of L, f9 be Function of A, the carrier of (L .: ) st f = f9 holds ( FinJoin (B,f)) = ( FinMeet (B,f9)) & ( FinMeet (B,f)) = ( FinJoin (B,f9));

    theorem :: LATTICE2:37



     Th37: for a9,b9 be Element of (L .: ) st a = a9 & b = b9 holds (a "/\" b) = (a9 "\/" b9) & (a "\/" b) = (a9 "/\" b9);

    theorem :: LATTICE2:38



     Th38: a [= b implies for a9,b9 be Element of (L .: ) st a = a9 & b = b9 holds b9 [= a9

    proof

      assume a [= b;

      then

       A1: (a "\/" b) = b;

      let a9,b9 be Element of (L .: );

      assume a = a9 & b = b9;

      then (b9 "/\" a9) = b9 by A1, Th37;

      hence thesis by LATTICES: 4;

    end;

    theorem :: LATTICE2:39



     Th39: for a9,b9 be Element of (L .: ) st a9 [= b9 & a = a9 & b = b9 holds b [= a

    proof

      let a9,b9 be Element of (L .: );

      assume that

       A1: a9 [= b9 and

       A2: a = a9 & b = b9;

      (a9 "\/" b9) = b9 by A1;

      then (b "/\" a) = b by A2, Th37;

      hence thesis by LATTICES: 4;

    end;

    theorem :: LATTICE2:40



     Th40: x in B implies ( FinMeet (B,f)) [= (f . x)

    proof

      reconsider f9 = f as Function of A, the carrier of (L .: );

      assume x in B;

      then (f9 . x) [= ( FinJoin (B,f9)) by Th28;

      hence thesis by Th39;

    end;

    theorem :: LATTICE2:41



     Th41: (ex x st x in B & (f . x) [= u) implies ( FinMeet (B,f)) [= u

    proof

      given x such that

       A1: x in B and

       A2: (f . x) [= u;

      reconsider u9 = u as Element of (L .: );

      reconsider f9 = f as Function of A, the carrier of (L .: );

      u9 [= (f9 . x) by A2, Th38;

      then u9 [= ( FinJoin (B,f9)) by A1, Th29;

      hence thesis by Th39;

    end;

    theorem :: LATTICE2:42

    (for x st x in B holds (f . x) = u) & B <> {} implies ( FinMeet (B,f)) = u by SETWISEO: 24;

    theorem :: LATTICE2:43

    B <> {} implies (v "/\" ( FinMeet (B,f))) = ( FinMeet (B,(the L_meet of L [;] (v,f)))) by Th25, SETWISEO: 27;

    theorem :: LATTICE2:44

    u [= ( FinMeet (B,f)) implies for x st x in B holds u [= (f . x)

    proof

      assume

       A1: u [= ( FinMeet (B,f));

      let x;

      assume x in B;

      then ( FinMeet (B,f)) [= (f . x) by Th40;

      hence thesis by A1, LATTICES: 7;

    end;

    theorem :: LATTICE2:45

    B <> {} & (f | B) = (g | B) implies ( FinMeet (B,f)) = ( FinMeet (B,g))

    proof

      reconsider f9 = f, g9 = g as Function of A, the carrier of (L .: );



       A1: ( FinMeet (B,f)) = ( FinJoin (B,f9)) & ( FinMeet (B,g)) = ( FinJoin (B,g9));

      assume B <> {} & (f | B) = (g | B);

      hence thesis by A1, Th34;

    end;

    theorem :: LATTICE2:46



     Th46: B <> {} & (for x st x in B holds u [= (f . x)) implies u [= ( FinMeet (B,f))

    proof

      assume that

       A1: B <> {} and

       A2: for x st x in B holds u [= (f . x);

      reconsider u9 = u as Element of (L .: );

      reconsider f9 = f as Function of A, the carrier of (L .: );

      for x st x in B holds (f9 . x) [= u9 by A2, Th38;

      then ( FinJoin (B,f9)) [= u9 by A1, Th32;

      hence thesis by Th39;

    end;

    theorem :: LATTICE2:47

    B <> {} & (for x st x in B holds (f . x) [= (g . x)) implies ( FinMeet (B,f)) [= ( FinMeet (B,g))

    proof

      assume that

       A1: B <> {} and

       A2: for x st x in B holds (f . x) [= (g . x);

      now

        let x;

        assume

         A3: x in B;

        then (f . x) [= (g . x) by A2;

        hence ( FinMeet (B,f)) [= (g . x) by A3, Th41;

      end;

      hence thesis by A1, Th46;

    end;

    theorem :: LATTICE2:48

    for L be Lattice holds L is lower-bounded iff (L .: ) is upper-bounded

    proof

      let L be Lattice;

      thus L is lower-bounded implies (L .: ) is upper-bounded

      proof

        given c be Element of L such that

         A1: for a be Element of L holds (c "/\" a) = c & (a "/\" c) = c;

        reconsider c9 = c as Element of (L .: );

        take c9;

        let a9 be Element of (L .: );

        reconsider a = a9 as Element of L;



        thus (c9 "\/" a9) = (c "/\" a)

        .= c9 by A1;

        hence (a9 "\/" c9) = c9;

      end;

      given c be Element of (L .: ) such that

       A2: for a be Element of (L .: ) holds (c "\/" a) = c & (a "\/" c) = c;

      reconsider c9 = c as Element of L;

      take c9;

      let a9 be Element of L;

      reconsider a = a9 as Element of (L .: );



      thus (c9 "/\" a9) = (c "\/" a)

      .= c9 by A2;

      hence (a9 "/\" c9) = c9;

    end;

    theorem :: LATTICE2:49



     Th49: for L be Lattice holds L is upper-bounded iff (L .: ) is lower-bounded

    proof

      let L be Lattice;

      thus L is upper-bounded implies (L .: ) is lower-bounded

      proof

        given c be Element of L such that

         A1: for a be Element of L holds (c "\/" a) = c & (a "\/" c) = c;

        reconsider c9 = c as Element of (L .: );

        take c9;

        let a9 be Element of (L .: );

        reconsider a = a9 as Element of L;



        thus (c9 "/\" a9) = (c "\/" a)

        .= c9 by A1;

        hence (a9 "/\" c9) = c9;

      end;

      given c be Element of (L .: ) such that

       A2: for a be Element of (L .: ) holds (c "/\" a) = c & (a "/\" c) = c;

      reconsider c9 = c as Element of L;

      take c9;

      let a9 be Element of L;

      reconsider a = a9 as Element of (L .: );



      thus (c9 "\/" a9) = (c "/\" a)

      .= c9 by A2;

      hence (a9 "\/" c9) = c9;

    end;

    theorem :: LATTICE2:50

    L is D_Lattice iff (L .: ) is D_Lattice by Th22, Th23;

    reserve L for 0_Lattice,

f,g for Function of A, the carrier of L,

u for Element of L;

    theorem :: LATTICE2:51



     Th51: ( Bottom L) is_a_unity_wrt the L_join of L

    proof

      now

        let u;



        thus (the L_join of L . (( Bottom L),u)) = (( Bottom L) "\/" u)

        .= u;

      end;

      hence thesis by BINOP_1: 4;

    end;

    registration

      let L;

      cluster the L_join of L -> having_a_unity;

      coherence

      proof

        ( Bottom L) is_a_unity_wrt the L_join of L by Th51;

        hence thesis;

      end;

    end

    theorem :: LATTICE2:52

    ( Bottom L) = ( the_unity_wrt the L_join of L) by Th18;

    theorem :: LATTICE2:53



     Th53: (f | B) = (g | B) implies ( FinJoin (B,f)) = ( FinJoin (B,g))

    proof

      set J = the L_join of L;



       A1: ( Bottom L) = ( the_unity_wrt J) by Th18;

      assume

       A2: (f | B) = (g | B);

      now

        per cases ;

          suppose

           A3: B = {} ;



          hence ( FinJoin (B,f)) = (J $$ (( {}. A),f))

          .= ( Bottom L) by A1, SETWISEO: 31

          .= (J $$ (( {}. A),g)) by A1, SETWISEO: 31

          .= ( FinJoin (B,g)) by A3;

        end;

          suppose B <> {} ;

          hence thesis by A2, Th34;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATTICE2:54



     Th54: (for x st x in B holds (f . x) [= u) implies ( FinJoin (B,f)) [= u

    proof

      assume

       A1: for x st x in B holds (f . x) [= u;

      set J = the L_join of L;



       A2: ( Bottom L) = ( the_unity_wrt J) by Th18;

      now

        per cases ;

          suppose B = {} ;



          then ( FinJoin (B,f)) = (J $$ (( {}. A),f))

          .= ( Bottom L) by A2, SETWISEO: 31;

          hence thesis;

        end;

          suppose B <> {} ;

          hence thesis by A1, Th32;

        end;

      end;

      hence thesis;

    end;

    theorem :: LATTICE2:55

    (for x st x in B holds (f . x) [= (g . x)) implies ( FinJoin (B,f)) [= ( FinJoin (B,g))

    proof

      assume

       A1: for x st x in B holds (f . x) [= (g . x);

      now

        let x;

        assume

         A2: x in B;

        then (f . x) [= (g . x) by A1;

        hence (f . x) [= ( FinJoin (B,g)) by A2, Th29;

      end;

      hence thesis by Th54;

    end;

    reserve L for 1_Lattice,

f,g for Function of A, the carrier of L,

u for Element of L;

    theorem :: LATTICE2:56



     Th56: ( Top L) is_a_unity_wrt the L_meet of L

    proof

      now

        let u;



        thus (the L_meet of L . (( Top L),u)) = (( Top L) "/\" u)

        .= u;

      end;

      hence thesis by BINOP_1: 4;

    end;

    registration

      let L;

      cluster the L_meet of L -> having_a_unity;

      coherence

      proof

        ( Top L) is_a_unity_wrt the L_meet of L by Th56;

        hence thesis;

      end;

    end

    theorem :: LATTICE2:57

    ( Top L) = ( the_unity_wrt the L_meet of L) by Th19;

    theorem :: LATTICE2:58

    (f | B) = (g | B) implies ( FinMeet (B,f)) = ( FinMeet (B,g))

    proof

      assume

       A1: (f | B) = (g | B);

      reconsider f9 = f, g9 = g as Function of A, the carrier of (L .: );



       A2: ( FinMeet (B,g)) = ( FinJoin (B,g9));

      (L .: ) is 0_Lattice & ( FinMeet (B,f)) = ( FinJoin (B,f9)) by Th49;

      hence thesis by A1, A2, Th53;

    end;

    theorem :: LATTICE2:59



     Th59: (for x st x in B holds u [= (f . x)) implies u [= ( FinMeet (B,f))

    proof

      reconsider f9 = f as Function of A, the carrier of (L .: );

      reconsider u9 = u as Element of (L .: );

      assume for x st x in B holds u [= (f . x);

      then

       A1: for x st x in B holds (f9 . x) [= u9 by Th38;

      (L .: ) is 0_Lattice by Th49;

      then ( FinJoin (B,f9)) [= u9 by A1, Th54;

      hence thesis by Th39;

    end;

    theorem :: LATTICE2:60

    (for x st x in B holds (f . x) [= (g . x)) implies ( FinMeet (B,f)) [= ( FinMeet (B,g))

    proof

      assume

       A1: for x st x in B holds (f . x) [= (g . x);

      now

        let x;

        assume

         A2: x in B;

        then (f . x) [= (g . x) by A1;

        hence ( FinMeet (B,f)) [= (g . x) by A2, Th41;

      end;

      hence thesis by Th59;

    end;

    theorem :: LATTICE2:61

    for L be 0_Lattice holds ( Bottom L) = ( Top (L .: ))

    proof

      let L be 0_Lattice;

      reconsider u = ( Bottom L) as Element of (L .: );

      now

        let v be Element of (L .: );

        reconsider v9 = v as Element of L;



        thus (v "\/" u) = (( Bottom L) "/\" v9) by Th37

        .= u;

      end;

      hence thesis by RLSUB_2: 65;

    end;

    theorem :: LATTICE2:62

    for L be 1_Lattice holds ( Top L) = ( Bottom (L .: ))

    proof

      let L be 1_Lattice;

      reconsider u = ( Top L) as Element of (L .: );

      now

        let v be Element of (L .: );

        reconsider v9 = v as Element of L;



        thus (v "/\" u) = (( Top L) "\/" v9) by Th37

        .= u;

      end;

      hence thesis by RLSUB_2: 64;

    end;

    definition

      mode D0_Lattice is distributive lower-bounded Lattice;

    end

    reserve L for D0_Lattice,

f,g for Function of A, the carrier of L,

u for Element of L;

    theorem :: LATTICE2:63

    the L_meet of L is_distributive_wrt the L_join of L by Th23;

    theorem :: LATTICE2:64



     Th64: (the L_meet of L . (u,( FinJoin (B,f)))) = ( FinJoin (B,(the L_meet of L [;] (u,f))))

    proof



       A1: (the L_meet of L . (u,( Bottom L))) = (u "/\" ( Bottom L))

      .= ( Bottom L);

      the L_meet of L is_distributive_wrt the L_join of L & ( Bottom L) = ( the_unity_wrt the L_join of L) by Th18, Th23;

      hence thesis by A1, SETWOP_2: 12;

    end;

    theorem :: LATTICE2:65

    (for x st x in B holds (g . x) = (u "/\" (f . x))) implies (u "/\" ( FinJoin (B,f))) = ( FinJoin (B,g))

    proof

      reconsider G = ((the L_meet of L [;] (u,f)) +* (g | B)) as Function of A, the carrier of L by Th3;

      ( dom (g | B)) = B by Th9;

      then

       A1: (G | B) = (g | B) by FUNCT_4: 23;

      assume

       A2: for x st x in B holds (g . x) = (u "/\" (f . x));

      now

        let x;

        assume x in B;



        hence (g . x) = (u "/\" (f . x)) by A2

        .= ((the L_meet of L [;] (u,f)) . x) by FUNCOP_1: 53;

      end;

      then G = (the L_meet of L [;] (u,f)) by Th10;



      hence (u "/\" ( FinJoin (B,f))) = ( FinJoin (B,G)) by Th64

      .= ( FinJoin (B,g)) by A1, Th53;

    end;

    theorem :: LATTICE2:66

    (u "/\" ( FinJoin (B,f))) = ( FinJoin (B,(the L_meet of L [;] (u,f)))) by Th64;

    definition

      let IT be Lattice;

      :: LATTICE2:def5

      attr IT is Heyting means IT is implicative lower-bounded;

    end

    registration

      cluster Heyting for Lattice;

      existence

      proof

        set L = the B_Lattice;

        take L;

        thus L is implicative lower-bounded;

      end;

    end

    registration

      cluster Heyting -> implicative lower-bounded for Lattice;

      coherence ;

      cluster implicative lower-bounded -> Heyting for Lattice;

      coherence ;

    end

    definition

      mode H_Lattice is Heyting Lattice;

    end

    registration

      cluster Heyting strict for Lattice;

      existence

      proof

        set L = the strict B_Lattice;

        L is I_Lattice;

        hence thesis;

      end;

    end

    theorem :: LATTICE2:67

    for L be 0_Lattice holds L is H_Lattice iff for x,z be Element of L holds ex y be Element of L st (x "/\" y) [= z & for v be Element of L st (x "/\" v) [= z holds v [= y

    proof

      let L be 0_Lattice;

      L is H_Lattice iff L is I_Lattice;

      hence thesis by FILTER_0:def 6;

    end;

    theorem :: LATTICE2:68

    for L be Lattice holds L is finite iff (L .: ) is finite;

    registration

      cluster finite -> lower-bounded for Lattice;

      coherence

      proof

        let L be Lattice;

        assume L is finite;

        then

        reconsider B = the carrier of L as Element of ( Fin the carrier of L) by FINSUB_1:def 5;

        take c = ( FinMeet (B,( id the carrier of L)));

        let a be Element of L;

        (( id the carrier of L) . a) [= a;

        then

         A1: c [= a by Th41;

        hence (c "/\" a) = c by LATTICES: 4;

        thus (a "/\" c) = c by A1, LATTICES: 4;

      end;

      cluster finite -> upper-bounded for Lattice;

      coherence

      proof

        let L be Lattice;

        assume L is finite;

        then

        reconsider B = the carrier of L as Element of ( Fin the carrier of L) by FINSUB_1:def 5;

        take c = ( FinJoin (B,( id the carrier of L)));

        let a be Element of L;

        a [= (( id the carrier of L) . a);

        then

         A2: a [= c by Th29;

        hence (c "\/" a) = c;

        thus (a "\/" c) = c by A2;

      end;

    end

    registration

      cluster finite -> bounded for Lattice;

      coherence ;

    end

    registration

      cluster distributive finite -> Heyting for Lattice;

      coherence

      proof

        let L be Lattice;

        assume

         A1: L is distributive finite;

        then

        reconsider L as D0_Lattice;

        set C = the carrier of L;

        L is implicative

        proof

          let p,q be Element of C;

          defpred X[ Element of C] means (p "/\" $1) [= q;

          set B = { x where x be Element of C : X[x] };



           A2: B c= C from FRAENKEL:sch 10;

          then B is finite by A1, FINSET_1: 1;

          then

          reconsider B as Element of ( Fin C) by A2, FINSUB_1:def 5;

          take r = ( FinJoin (B,( id C)));

           A3:

          now

            let x be Element of C;

            assume x in B;

            then

             A4: ex x9 be Element of C st x9 = x & (p "/\" x9) [= q;

            ((the L_meet of L [;] (p,( id C))) . x) = (the L_meet of L . (p,(( id C) . x))) by FUNCOP_1: 53

            .= (p "/\" x);

            hence ((the L_meet of L [;] (p,( id C))) . x) [= q by A4;

          end;

          (p "/\" r) = ( FinJoin (B,(the L_meet of L [;] (p,( id C))))) by Th64;

          hence (p "/\" r) [= q by A3, Th54;

          let r1 be Element of C;

          assume (p "/\" r1) [= q;

          then

           A5: r1 in B;

          r1 = (( id C) . r1);

          hence r1 [= r by A5, Th28;

        end;

        hence thesis;

      end;

    end