LATTICE2

:: Finite Join and Finite Meet, and Dual Lattices
::  by Andrzej Trybulec
::
:: Received August 10, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4, TARSKI, FINSUB_1,
      BINOP_1, LATTICES, EQREL_1, STRUCT_0, PBOOLE, SETWISEO, FUNCOP_1,
      FILTER_0, FINSET_1, XXREAL_2, LATTICE2;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4,
      PARTFUN1, FUNCOP_1, BINOP_1, FINSET_1, STRUCT_0, LATTICES, FINSUB_1,
      SETWISEO, FILTER_0;
 constructors BINOP_1, FUNCOP_1, FUNCT_4, SETWISEO, GROUP_1, FILTER_0,
      RELSET_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES,
      FILTER_0;
 requirements SUBSET, BOOLE;
 definitions LATTICES, BINOP_1, SETWISEO, FILTER_0;
 equalities LATTICES;
 expansions LATTICES, BINOP_1, SETWISEO;
 theorems LATTICES, BINOP_1, SETWISEO, FUNCOP_1, FUNCT_4, SETWOP_2, FINSET_1,
      FINSUB_1, FUNCT_2, FUNCT_1, FILTER_0, GRFUNC_1, RELAT_1, RLSUB_2,
      XBOOLE_1;
 schemes FRAENKEL;

begin :: Auxiliary theorems

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 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 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 Th3:
  for B being 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 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 Th5:
  for f,g being 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
  f +* f|B = f by Th5,RELAT_1:59;

theorem 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
  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 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 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;
  pred o absorbs o9 means

  for x,y being 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;

:: Dual Lattice structures

reserve L for non empty LattStr,
  a,b,c for Element of L;

theorem 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;
  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
  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
  for L being strict non empty LattStr holds L .: .: = L;

:: General Lattices

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

theorem 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 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 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 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 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 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 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
  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 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 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
  the L_meet of L is_distributive_wrt the L_join of L implies L is distributive
by BINOP_1:12;

theorem 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 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 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;
  func FinJoin(B, f) -> Element of L equals
  (the L_join of L)$$(B,f);
  correctness;
  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 Th28:
  x in B implies f.x [= FinJoin(B,f)
by SETWISEO:22;

theorem 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
  (for x st x in B holds f.x = u) & B <> {} implies FinJoin(B,f) = u by
SETWISEO:24;

theorem
  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 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
  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 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
  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
  for L being Lattice, B being Element of Fin A for f being Function
  of A, the carrier of L, f9 being Function of A, the carrier of L.: st f = f9
  holds FinJoin(B,f) = FinMeet(B,f9) & FinMeet(B,f) = FinJoin(B,f9);

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

theorem Th38:
  a [= b implies for a9,b9 being 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 Th39:
  for a9,b9 being 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;

:: Dualizations

theorem 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 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
  (for x st x in B holds f.x = u) & B <> {} implies FinMeet(B,f) = u
  by SETWISEO:24;

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

theorem
  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
  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 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
  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
  for L being 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 being Element of L such that
A1: for a being 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 being Element of L.: such that
A2: for a being 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 Th49:
  for L being 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 being Element of L such that
A1: for a being 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 being Element of L.: such that
A2: for a being 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
  L is D_Lattice iff L.: is D_Lattice by Th22,Th23;

::
:: Lower bounded lattices
::

reserve L for 0_Lattice,
  f,g for Function of A, the carrier of L,
  u for Element of L;

theorem 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
  Bottom L = the_unity_wrt the L_join of L by Th18;

theorem 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 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
  (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;

::
:: Upper bounded lattices
::

reserve L for 1_Lattice,
  f,g for Function of A, the carrier of L,
  u for Element of L;

theorem 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
  Top L = the_unity_wrt the L_meet of L by Th19;

theorem
  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 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
  (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
  for L being 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
  for L being 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;

::
:: Distributive lattices with the minimal element
::

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
  the L_meet of L is_distributive_wrt the L_join of L by Th23;

theorem 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
  (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
  u "/\" FinJoin(B,f) = FinJoin(B, (the L_meet of L)[;](u, f)) by Th64;

:: Heyting Lattices

definition
  let IT be Lattice;

  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
  for L being 0_Lattice holds L is H_Lattice iff for x,z being Element
  of L ex y being Element of L st x "/\" y [= z & for v being 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
  for L being 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 is 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 being 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;