The abstract of the Mizar article:

Galois Connections

by

Czeslaw Bylinski

Received September 25, 1996

MML identifier: WAYBEL_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, PRE_TOPC, ORDERS_1, SEQM_3, RELAT_2, LATTICE3,
      LATTICES, WAYBEL_0, YELLOW_1, BOOLE, YELLOW_0, CAT_1, WELLORD1, ORDINAL2,
      BHSP_3, FILTER_0, FILTER_2, BINOP_1, SGRAPH1, GROUP_6, QUANTAL1,
      YELLOW_2, LATTICE2, ZF_LANG, FILTER_1, WAYBEL_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      PRE_TOPC, STRUCT_0, WELLORD1, ORDERS_1, LATTICE3, QUANTAL1, ORDERS_3,
      YELLOW_0, GRCAT_1, YELLOW_1, WAYBEL_0, YELLOW_2;
 constructors TOPS_2, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, GRCAT_1;
 clusters STRUCT_0, RELSET_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0,
      RELAT_1, FUNCT_2, PARTFUN1;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

definition let L1,L2 be non empty 1-sorted, f be map of L1,L2;
 redefine attr f is one-to-one means
:: WAYBEL_1:def 1
     for x,y being Element of L1 st f.x = f.y holds x=y;
end;

theorem :: WAYBEL_1:1
  for L being non empty 1-sorted, f being map of L,L
    st for x being Element of L holds f.x = x
   holds f = id L;

definition let L1,L2 be non empty RelStr, f be map of L1,L2;
 redefine attr f is monotone means
:: WAYBEL_1:def 2
 for x,y being Element of L1 st x <= y holds f.x <= f.y;
end;

theorem :: WAYBEL_1:2
   for L being antisymmetric transitive with_infima RelStr,
       x,y,z being Element of L
     st x <= y holds x "/\" z <= y "/\" z;

theorem :: WAYBEL_1:3
   for L being antisymmetric transitive with_suprema RelStr,
       x,y,z being Element of L
     st x <= y holds x "\/" z <= y "\/" z;

theorem :: WAYBEL_1:4
 for L being non empty lower-bounded antisymmetric RelStr
  for x being Element of L holds
 (L is with_infima implies Bottom L "/\" x = Bottom L) &
 (L is with_suprema reflexive transitive implies Bottom L "\/" x = x);

theorem :: WAYBEL_1:5
 for L being non empty upper-bounded antisymmetric RelStr
  for x being Element of L holds
 (L is with_infima transitive reflexive implies Top L "/\" x = x) &
 (L is with_suprema implies Top L "\/" x = Top L);

definition let L be non empty RelStr;
 attr L is distributive means
:: WAYBEL_1:def 3
 for x,y,z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/"
 (x "/\" z);
end;

theorem :: WAYBEL_1:6
   for L being LATTICE
    holds L is distributive iff
     for x,y,z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x
"\/" z);

definition let X be set;
 cluster BoolePoset X -> distributive;
end;


definition let S be non empty RelStr, X be set;
  pred ex_min_of X,S means
:: WAYBEL_1:def 4
    ex_inf_of X,S & "/\"(X,S) in X;
   synonym X has_the_min_in S;
  pred ex_max_of X,S means
:: WAYBEL_1:def 5
  ex_sup_of X,S & "\/"(X,S) in X;
   synonym X has_the_max_in S;
end;

definition
 let S be non empty RelStr, s be Element of S, X be set;
  pred s is_minimum_of X means
:: WAYBEL_1:def 6
  ex_inf_of X,S & s = "/\"(X,S) & "/\"(X,S) in X;
  pred s is_maximum_of X means
:: WAYBEL_1:def 7
  ex_sup_of X,S & s = "\/"(X,S) & "\/"(X,S)in X;
end;

definition let L be RelStr;
 cluster id L -> isomorphic;
end;

definition let L1,L2 be RelStr;
 pred L1,L2 are_isomorphic means
:: WAYBEL_1:def 8
  ex f being map of L1,L2 st f is isomorphic;
 reflexivity;
end;

theorem :: WAYBEL_1:7
     for L1,L2 be non empty RelStr st L1,L2 are_isomorphic
    holds L2,L1 are_isomorphic;

theorem :: WAYBEL_1:8
     for L1,L2,L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic
    holds L1,L3 are_isomorphic;

begin :: Galois Connections

definition let S,T be RelStr;
   mode Connection of S,T -> set means
:: WAYBEL_1:def 9
  ex g being map of S,T, d being map of T,S st it = [g,d];
end;

definition let S,T be RelStr, g be map of S,T, d be map of T,S;
 redefine func [g,d] -> Connection of S,T;
end;

:: Definition 3.1
definition let S,T be non empty RelStr, gc be Connection of S,T;
  attr gc is Galois means
:: WAYBEL_1:def 10
 ex g being map of S,T, d being map of T,S
    st gc = [g,d] & g is monotone & d is monotone &
     for t being Element of T, s being Element of S
      holds t <= g.s iff d.t <= s;
end;

theorem :: WAYBEL_1:9
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   holds [g,d] is Galois iff
     g is monotone & d is monotone &
      for t being Element of T, s being Element of S holds t <= g.s iff d.t <=
 s;

:: Definition 3.1
definition let S,T be non empty RelStr, g be map of S,T;
 attr g is upper_adjoint means
:: WAYBEL_1:def 11
  ex d being map of T,S st [g,d] is Galois;
 synonym g has_a_lower_adjoint;
end;

:: Definition 3.1
definition let S,T be non empty RelStr, d be map of T,S;
 attr d is lower_adjoint means
:: WAYBEL_1:def 12
  ex g being map of S,T st [g,d] is Galois;
 synonym d has_an_upper_adjoint;
end;

theorem :: WAYBEL_1:10
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   st [g,d] is Galois holds g is upper_adjoint & d is lower_adjoint;

:: Theorem 3.2  (1) iff (2)
theorem :: WAYBEL_1:11
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   holds [g,d] is Galois iff
    g is monotone &
     for t being Element of T holds d.t is_minimum_of g"(uparrow t);

:: Theorem 3.2 (1) iff (3)
theorem :: WAYBEL_1:12
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   holds [g,d] is Galois iff
     d is monotone &
      for s being Element of S holds g.s is_maximum_of d"(downarrow s);

:: Theorem 3.3 (first part)
theorem :: WAYBEL_1:13
  for S,T being non empty Poset,g being map of S,T st g is upper_adjoint
   holds g is infs-preserving;

definition let S,T be non empty Poset;
 cluster upper_adjoint -> infs-preserving map of S,T;
end;

:: Theorem 3.3 (second part)
theorem :: WAYBEL_1:14
  for S,T being non empty Poset, d being map of T,S st d is lower_adjoint
   holds d is sups-preserving;

definition let S,T be non empty Poset;
 cluster lower_adjoint -> sups-preserving map of S,T;
end;

:: Theorem 3.4
theorem :: WAYBEL_1:15
  for S,T being non empty Poset,g being map of S,T
    st S is complete & g is infs-preserving
   ex d being map of T,S st [g,d] is Galois &
    for t being Element of T holds d.t is_minimum_of g"(uparrow t);

:: Theorem 3.4 (dual)
theorem :: WAYBEL_1:16
  for S,T being non empty Poset, d being map of T,S
    st T is complete & d is sups-preserving
   ex g being map of S,T st [g,d] is Galois &
    for s being Element of S holds g.s is_maximum_of d"(downarrow s);

:: Corollary 3.5 (i)
theorem :: WAYBEL_1:17
    for S,T being non empty Poset, g being map of S,T
    st S is complete
   holds (g is infs-preserving iff g is monotone & g has_a_lower_adjoint);

:: Corollary 3.5 (ii)
theorem :: WAYBEL_1:18
  for S,T being non empty Poset, d being map of T,S
    st T is complete
   holds d is sups-preserving iff d is monotone & d has_an_upper_adjoint;

:: Theorem 3.6 (1) iff (2)
theorem :: WAYBEL_1:19
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
   st [g,d] is Galois holds d*g <= id S & id T <= g*d;

:: Theorem 3.6 (2) implies (1)
theorem :: WAYBEL_1:20
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st g is monotone & d is monotone & d*g <= id S & id T <= g*d
   holds [g,d] is Galois;

:: Theorem 3.6 (2) implies (3)
theorem :: WAYBEL_1:21
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st g is monotone & d is monotone & d*g <= id S & id T <= g*d
   holds d = d*g*d & g = g*d*g;

:: Theorem 3.6 (3) implies (4)
theorem :: WAYBEL_1:22
  for S,T being non empty RelStr, g being map of S,T, d being map of T,S
    st d = d*g*d & g = g*d*g
   holds g*d is idempotent & d*g is idempotent;

:: Proposition 3.7 (1) implies (2)
theorem :: WAYBEL_1:23
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st [g,d] is Galois & g is onto
   for t being Element of T holds d.t is_minimum_of g"{t};

:: Proposition 3.7 (2) implies (3)
theorem :: WAYBEL_1:24
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st for t being Element of T holds d.t is_minimum_of g"{t}
   holds g*d = id T;

:: Proposition 3.7 (3) implies (4)
theorem :: WAYBEL_1:25
   for L1,L2 being non empty 1-sorted,
       g1 being map of L1,L2, g2 being map of L2,L1
    st g2*g1 = id L1 holds g1 is one-to-one & g2 is onto;

:: Proposition 3.7 (4) iff (1)
theorem :: WAYBEL_1:26
    for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st [g,d] is Galois
   holds g is onto iff d is one-to-one;

:: Proposition 3.7 (1*) implies (2*)
theorem :: WAYBEL_1:27
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st [g,d] is Galois & d is onto
   for s being Element of S holds g.s is_maximum_of d"{s};

:: Proposition 3.7 (2*) implies (3*)
theorem :: WAYBEL_1:28
  for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st for s being Element of S holds g.s is_maximum_of d"{s}
   holds d*g = id S;

:: Proposition 3.7 (1*) iff (4*)
theorem :: WAYBEL_1:29
    for S,T being non empty Poset,g being map of S,T, d being map of T,S
    st [g,d] is Galois
   holds g is one-to-one iff d is onto;

:: Definition 3.8 (i)
definition let L be non empty RelStr, p be map of L,L;
  attr p is projection means
:: WAYBEL_1:def 13
 p is idempotent monotone;
  synonym p is_a_projection_operator;
end;

definition let L be non empty RelStr;
  cluster id L -> projection;
end;

definition let L be non empty RelStr;
 cluster projection map of L,L;
end;

:: Definition 3.8 (ii)
definition let L be non empty RelStr, c be map of L,L;
  attr c is closure means
:: WAYBEL_1:def 14
 c is projection & id(L) <= c;
 synonym c is_a_closure_operator;
end;

definition let L be non empty RelStr;
 cluster closure -> projection map of L,L;
end;

definition let L be non empty reflexive RelStr;
 cluster closure map of L,L;
end;

definition let L be non empty reflexive RelStr;
 cluster id L -> closure;
end;

:: Definition 3.8 (iii)
definition let L be non empty RelStr, k be map of L,L;
  attr k is kernel means
:: WAYBEL_1:def 15
 k is projection & k <= id(L);
 synonym k is_a_kernel_operator;
end;

definition let L be non empty RelStr;
 cluster kernel -> projection map of L,L;
end;

definition let L be non empty reflexive RelStr;
 cluster kernel map of L,L;
end;

definition let L be non empty reflexive RelStr;
 cluster id L -> kernel;
end;

theorem :: WAYBEL_1:30
  for L being non empty Poset, c being map of L,L, X being Subset of L
    st c is_a_closure_operator & ex_inf_of X,L & X c= rng c
   holds inf X = c.(inf X);

theorem :: WAYBEL_1:31
  for L being non empty Poset, k being map of L,L, X being Subset of L
    st k is_a_kernel_operator & ex_sup_of X,L & X c= rng k
   holds sup X = k.(sup X);

definition let L1, L2 be non empty RelStr, g be map of L1,L2;
 func corestr(g) -> map of L1,Image g equals
:: WAYBEL_1:def 16
  (the carrier of Image g)|g;
end;

theorem :: WAYBEL_1:32
  for L1, L2 being non empty RelStr,g being map of L1,L2 holds corestr g = g;

definition let L1, L2 be non empty RelStr, g be map of L1,L2;
 cluster corestr g -> onto;
end;

theorem :: WAYBEL_1:33
  for L1, L2 being non empty RelStr, g being map of L1,L2 st g is monotone
   holds corestr g is monotone;

definition let L1, L2 be non empty RelStr, g be map of L1,L2;
 func inclusion(g) -> map of Image g,L2 equals
:: WAYBEL_1:def 17
  id Image g;
end;

theorem :: WAYBEL_1:34
  for L1, L2 being non empty RelStr, g being map of L1,L2,
      s being Element of Image g
   holds (inclusion g).s = s;

definition let L1, L2 be non empty RelStr, g be map of L1,L2;
 cluster inclusion g -> one-to-one monotone;
end;

theorem :: WAYBEL_1:35
  for L being non empty RelStr, f being map of L,L
   holds (inclusion f)*(corestr f) = f;

::Theorem 3.10 (1) implies (2)
theorem :: WAYBEL_1:36
   for L being non empty Poset, f being map of L,L st f is idempotent
    holds (corestr f)*(inclusion f) = id(Image f);

::Theorem 3.10 (1) implies (3)
theorem :: WAYBEL_1:37
    for L being non empty Poset, f being map of L,L st f
is_a_projection_operator
    ex T being non empty Poset, q being map of L,T, i being map of T,L
      st q is monotone & q is onto & i is monotone & i is one-to-one &
         f = i*q & id(T) = q*i;

::Theorem 3.10 (3) implies (1)
theorem :: WAYBEL_1:38
     for L being non empty Poset, f being map of L,L
    st (ex T being non empty Poset, q being map of L,T, i being map of T,L
         st q is monotone & i is monotone & f = i*q & id(T) = q*i)
    holds f is_a_projection_operator;

::Theorem 3.10 (1_1) implies (2_1)
theorem :: WAYBEL_1:39
   for L being non empty Poset, f being map of L,L st f is_a_closure_operator
    holds [inclusion f,corestr f] is Galois;

::Theorem 3.10 (2_1) implies (3_1)
theorem :: WAYBEL_1:40
     for L being non empty Poset, f being map of L,L st f is_a_closure_operator
    ex S being non empty Poset, g being map of S,L, d being map of L,S
      st [g,d] is Galois & f = g*d;

::Theorem 3.10 (3_1) implies (1_1)
theorem :: WAYBEL_1:41
   for L being non empty Poset, f being map of L,L
      st f is monotone &
        ex S being non empty Poset, g being map of S,L, d being map of L,S
         st [g,d] is Galois & f = g*d
    holds f is_a_closure_operator;

::Theorem 3.10 (1_2) implies (2_2)
theorem :: WAYBEL_1:42
   for L being non empty Poset, f being map of L,L st f is_a_kernel_operator
    holds [corestr f,inclusion f] is Galois;

::Theorem 3.10 (2_2) implies (3_2)
theorem :: WAYBEL_1:43
     for L being non empty Poset, f being map of L,L st f is_a_kernel_operator
     ex T being non empty Poset, g being map of L,T, d being map of T,L
      st [g,d] is Galois & f = d*g;

::Theorem 3.10 (3_2) implies (1_2)
theorem :: WAYBEL_1:44
     for L being non empty Poset, f being map of L,L
    st f is monotone &
      ex T being non empty Poset, g being map of L,T, d being map of T,L
       st [g,d] is Galois & f = d*g
    holds f is_a_kernel_operator;

:: Lemma 3.11 (i) (part I)
theorem :: WAYBEL_1:45
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  holds rng p = {c where c is Element of L: c <= p.c} /\
                {k where k is Element of L: p.k <= k};

theorem :: WAYBEL_1:46
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  holds {c where c is Element of L: c <= p.c} is non empty Subset of L &
    {k where k is Element of L: p.k <= k} is non empty Subset of L;

:: Lemma 3.11 (i) (part II)
theorem :: WAYBEL_1:47
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  holds rng(p|{c where c is Element of L: c <= p.c}) = rng p &
    rng(p|{k where k is Element of L: p.k <= k}) = rng p;

theorem :: WAYBEL_1:48
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lc being non empty Subset of L, Lk being non empty Subset of L
   st Lc = {c where c is Element of L: c <= p.c}
  holds p|Lc is map of subrelstr Lc,subrelstr Lc;

theorem :: WAYBEL_1:49
    for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lk being non empty Subset of L
   st Lk = {k where k is Element of L: p.k <= k}
  holds p|Lk is map of subrelstr Lk,subrelstr Lk;

:: Lemma 3.11 (i) (part IIIa)
theorem :: WAYBEL_1:50
  for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lc being non empty Subset of L
   st Lc = {c where c is Element of L: c <= p.c}
  for pc being map of subrelstr Lc,subrelstr Lc st pc = p|Lc
   holds pc is_a_closure_operator;

:: Lemma 3.11 (i) (part IIIb)
theorem :: WAYBEL_1:51
    for L being non empty Poset, p being map of L,L
    st p is_a_projection_operator
   for Lk being non empty Subset of L
    st Lk = {k where k is Element of L: p.k <= k}
   for pk being map of subrelstr Lk,subrelstr Lk st pk = p|Lk
    holds pk is_a_kernel_operator;

:: Lemma 3.11 (ii) (part I)
theorem :: WAYBEL_1:52
  for L being non empty Poset, p being map of L,L st p is monotone
   for Lc being Subset of L st Lc = {c where c is Element of L: c <= p.c}
    holds subrelstr Lc is sups-inheriting;

:: Lemma 3.11 (ii) (part II)
theorem :: WAYBEL_1:53
  for L being non empty Poset, p being map of L,L st p is monotone
   for Lk being Subset of L st Lk = {k where k is Element of L: p.k <= k}
    holds subrelstr Lk is infs-inheriting;

:: Lemma 3.11 (iii) (part I)
theorem :: WAYBEL_1:54
    for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lc being non empty Subset of L
    st Lc = {c where c is Element of L: c <= p.c}
   holds
    (p is infs-preserving
      implies subrelstr Lc is infs-inheriting & Image p is infs-inheriting) &
    (p is filtered-infs-preserving
      implies subrelstr Lc is filtered-infs-inheriting &
              Image p is filtered-infs-inheriting);

:: Lemma 3.11 (iii) (part II)
theorem :: WAYBEL_1:55
    for L being non empty Poset, p being map of L,L
   st p is_a_projection_operator
  for Lk being non empty Subset of L
    st Lk = {k where k is Element of L: p.k <= k}
   holds
    (p is sups-preserving
      implies subrelstr Lk is sups-inheriting & Image p is sups-inheriting) &
    (p is directed-sups-preserving
      implies subrelstr Lk is directed-sups-inheriting &
              Image p is directed-sups-inheriting);

:: Proposition 3.12 (i)
theorem :: WAYBEL_1:56
  for L being non empty Poset, p being map of L,L holds
   (p is_a_closure_operator implies Image p is infs-inheriting) &
   (p is_a_kernel_operator implies Image p is sups-inheriting);

:: Proposition 3.12 (ii)
theorem :: WAYBEL_1:57
    for L being complete (non empty Poset), p being map of L,L
    st p is_a_projection_operator
   holds Image p is complete;

:: Proposition 3.12 (iii)
theorem :: WAYBEL_1:58
    for L being non empty Poset, c being map of L,L
    st c is_a_closure_operator
   holds corestr c is sups-preserving &
    for X being Subset of L
     st X c= the carrier of Image c & ex_sup_of X,L holds
      ex_sup_of X,Image c & "\/"(X,Image c) = c.("\/"(X,L));

:: Proposition 3.12 (iv)
theorem :: WAYBEL_1:59
    for L being non empty Poset, k being map of L,L
    st k is_a_kernel_operator
   holds (corestr k) is infs-preserving &
    for X being Subset of L
     st X c= the carrier of Image k & ex_inf_of X,L holds
      ex_inf_of X,Image k & "/\"(X,Image k) = k.("/\"(X,L));

begin :: Heyting algebras

:: Proposition 3.15 (i)
theorem :: WAYBEL_1:60
   for L being complete (non empty Poset)
    holds [IdsMap L,SupMap L] is Galois & SupMap L is sups-preserving;

:: Proposition 3.15 (ii)
theorem :: WAYBEL_1:61
     for L being complete (non empty Poset)
    holds (IdsMap L)*(SupMap L) is_a_closure_operator &
     Image ((IdsMap L)*(SupMap L)),L are_isomorphic;

definition let S be non empty RelStr; let x be Element of S;
 func x "/\" -> map of S,S means
:: WAYBEL_1:def 18
 for s being Element of S holds it.s = x"/\"s;
end;

theorem :: WAYBEL_1:62
  for S being non empty RelStr, x,t being Element of S
   holds {s where s is Element of S: x"/\"s <= t} = (x "/\")"(downarrow t);

theorem :: WAYBEL_1:63
  for S being Semilattice, x be Element of S
   holds x "/\" is monotone;

definition let S be Semilattice, x be Element of S;
 cluster x "/\" -> monotone;
end;

theorem :: WAYBEL_1:64
   for S being non empty RelStr, x being Element of S, X being Subset of S
    holds (x "/\").:X = {x"/\"y where y is Element of S: y in X};

:: Lemma 3.16 (1) iff (2)
theorem :: WAYBEL_1:65
  for S being Semilattice
   holds (for x being Element of S holds x "/\" has_an_upper_adjoint)
    iff (for x,t being Element of S
         holds ex_max_of {s where s is Element of S: x"/\"s <= t},S);

:: Lemma 3.16 (1) implies (3)
theorem :: WAYBEL_1:66
  for S being Semilattice
    st for x being Element of S holds x "/\" has_an_upper_adjoint
   for X being Subset of S st ex_sup_of X,S
    for x being Element of S holds
     x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S);

:: Lemma 3.16 (1) iff (3)
theorem :: WAYBEL_1:67
    for S being complete (non empty Poset) holds
    (for x being Element of S holds x "/\" has_an_upper_adjoint)
   iff for X being Subset of S, x being Element of S
     holds x "/\" "\/"(X,S) = "\/"({x"/\"y where y is Element of S: y in X},S);

:: Lemma 3.16 (3) implies (D)
theorem :: WAYBEL_1:68
  for S being LATTICE
   st for X being Subset of S st ex_sup_of X,S for x being Element of S
       holds x"/\"("\/"(X,S)) = "\/"({x"/\"
y where y is Element of S: y in X},S)
   holds S is distributive;

definition let H be non empty RelStr;
 attr H is Heyting means
:: WAYBEL_1:def 19
 H is LATTICE & for x being Element of H holds x "/\"
has_an_upper_adjoint;
 synonym H is_a_Heyting_algebra;
end;

definition
 cluster Heyting -> with_infima with_suprema
                     reflexive transitive antisymmetric (non empty RelStr);
end;

definition let H be non empty RelStr, a be Element of H;
 assume
 H is Heyting;
 func a => -> map of H,H means
:: WAYBEL_1:def 20
 [it,a "/\"] is Galois;
end;

theorem :: WAYBEL_1:69
   for H being non empty RelStr st H is_a_Heyting_algebra
    holds H is distributive;

definition
 cluster Heyting -> distributive (non empty RelStr);
end;

definition let H be non empty RelStr, a,y be Element of H;
 func a => y -> Element of H equals
:: WAYBEL_1:def 21
  (a=>).y;
end;

theorem :: WAYBEL_1:70
   for H being non empty RelStr st H is_a_Heyting_algebra
    for x,a,y being Element of H holds x >= a "/\" y iff a => x >= y;

theorem :: WAYBEL_1:71
   for H being non empty RelStr st H is_a_Heyting_algebra
    holds H is upper-bounded;

definition
 cluster Heyting -> upper-bounded (non empty RelStr);
end;

theorem :: WAYBEL_1:72
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds Top H = a => b iff a <= b;

theorem :: WAYBEL_1:73
     for H being non empty RelStr st H is_a_Heyting_algebra
    for a being Element of H holds Top H = a => a;

theorem :: WAYBEL_1:74
     for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H st Top H = a => b & Top H = b => a holds a = b;

theorem :: WAYBEL_1:75
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds b <= (a => b);

theorem :: WAYBEL_1:76
     for H being non empty RelStr st H is_a_Heyting_algebra
    for a being Element of H holds Top H = a => Top H;

theorem :: WAYBEL_1:77
     for H being non empty RelStr st H is_a_Heyting_algebra
    for b being Element of H holds b = (Top H) => b;

theorem :: WAYBEL_1:78
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b,c being Element of H st a <= b holds (b => c) <= (a => c);

theorem :: WAYBEL_1:79
     for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b,c being Element of H st b <= c holds (a => b) <= (a => c);

theorem :: WAYBEL_1:80
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds a"/\"(a => b) = a"/\"b;

theorem :: WAYBEL_1:81
   for H being non empty RelStr st H is_a_Heyting_algebra
    for a,b,c being Element of H holds (a"\/"b)=> c = (a => c) "/\" (b => c);

definition let H be non empty RelStr, a be Element of H;
  func 'not' a -> Element of H equals
:: WAYBEL_1:def 22
  a => Bottom H;
end;

theorem :: WAYBEL_1:82
     for H being non empty RelStr st H is_a_Heyting_algebra & H is
lower-bounded
    for a being Element of H
     holds 'not' a is_maximum_of {x where x is Element of H: a"/\"x = Bottom H}
;

theorem :: WAYBEL_1:83
   for H being non empty RelStr st H is_a_Heyting_algebra & H is lower-bounded
    holds 'not' Bottom H = Top H & 'not' Top H = Bottom H;

:: Exercise 3.18 (i)
theorem :: WAYBEL_1:84
     for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
     for a,b being Element of H holds 'not' a >= b iff 'not' b >= a;

:: Exercise 3.18 (ii)
theorem :: WAYBEL_1:85
   for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
     for a,b being Element of H holds 'not' a >= b iff a "/\" b = Bottom H;

theorem :: WAYBEL_1:86
     for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
     for a,b being Element of H st a <= b holds 'not' b <= 'not' a;

theorem :: WAYBEL_1:87
   for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds 'not' (a"\/"b) = 'not' a"/\"'not' b;

theorem :: WAYBEL_1:88
     for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra
    for a,b being Element of H holds 'not' (a"/\"b) >= 'not' a"\/"'not' b;

definition let L be non empty RelStr, x,y be Element of L;
 pred y is_a_complement_of x means
:: WAYBEL_1:def 23
 x "\/" y = Top L & x "/\" y = Bottom L;
end;

definition let L be non empty RelStr;
 attr L is complemented means
:: WAYBEL_1:def 24

  for x being Element of L ex y being Element of L st y is_a_complement_of x;
end;

definition let X be set;
 cluster BoolePoset X -> complemented;
end;

:: Exercise 3.19
theorem :: WAYBEL_1:89
   for L being bounded LATTICE
    st L is_a_Heyting_algebra & for x being Element of L holds
    'not' 'not' x = x
   for x being Element of L holds 'not' x is_a_complement_of x;

:: Exercise 3.19  (1) iff (2)
theorem :: WAYBEL_1:90
   for L being bounded LATTICE
    holds L is distributive complemented
      iff L is_a_Heyting_algebra & for x being Element of L holds 'not' 'not'
 x = x;

:: Definition 3.20
definition let B be non empty RelStr;
 attr B is Boolean means
:: WAYBEL_1:def 25
 B is LATTICE & B is bounded distributive complemented;
  synonym B is_a_Boolean_algebra;
  synonym B is_a_Boolean_lattice;
end;

definition
 cluster Boolean -> reflexive transitive antisymmetric with_infima with_suprema
    bounded distributive complemented (non empty RelStr);
end;

definition
 cluster reflexive transitive antisymmetric with_infima with_suprema
    bounded distributive complemented -> Boolean (non empty RelStr);
end;

definition
 cluster Boolean -> Heyting (non empty RelStr);
end;

definition
 cluster strict Boolean non empty LATTICE;
end;

definition
 cluster strict Heyting non empty LATTICE;
end;