Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### Galois Connections

by
Czeslaw Bylinski

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;
:: WAYBEL_1:def 11
ex d being map of T,S st [g,d] is Galois;
end;

:: Definition 3.1
definition let S,T be non empty RelStr, d be map of T,S;
:: WAYBEL_1:def 12
ex g being map of S,T st [g,d] is Galois;
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 "/\"
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;

```