:: Galois Connections
:: by Czes\law Byli\'nski
::
:: Received September 25, 1996
:: Copyright (c) 1996-2018 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, STRUCT_0, FUNCT_1, SUBSET_1, ORDERS_2, SEQM_3,
XXREAL_0, RELAT_2, LATTICE3, LATTICES, EQREL_1, WAYBEL_0, YELLOW_1,
YELLOW_0, RELAT_1, CAT_1, WELLORD1, ORDINAL2, TARSKI, REWRITE1, CARD_FIL,
BINOP_1, FUNCT_2, GROUP_6, YELLOW_2, LATTICE2, XBOOLEAN, ZFMISC_1,
XXREAL_2, WAYBEL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
DOMAIN_1, STRUCT_0, WELLORD1, ORDERS_2, LATTICE3, QUANTAL1, ORDERS_3,
YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_2;
constructors DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, YELLOW_2, RELSET_1;
registrations RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_1, YELLOW_2, RELSET_1;
requirements SUBSET, BOOLE;
begin :: Preliminaries
definition
let L1,L2 be non empty 1-sorted, f be Function 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;
definition
let L1,L2 be non empty RelStr, f be Function 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:1
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:2
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:3
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:4
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:5
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);
registration
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;
pred ex_max_of X,S means
:: WAYBEL_1:def 5
ex_sup_of X,S & "\/"(X,S) in X;
end;
notation
let S be non empty RelStr, X be set;
synonym X has_the_min_in S for ex_min_of X,S;
synonym X has_the_max_in S for ex_max_of X,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;
registration
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 Function of L1,L2 st f is isomorphic;
reflexivity;
end;
theorem :: WAYBEL_1:6
for L1,L2 be non empty RelStr st L1,L2 are_isomorphic holds L2,L1
are_isomorphic;
theorem :: WAYBEL_1:7
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 Function of S,T, d being Function of T,S st it = [g,d];
end;
definition
let S,T be RelStr, g be Function of S,T, d be Function 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 Function of S,T, d being Function
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:8
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of S,T;
attr g is upper_adjoint means
:: WAYBEL_1:def 11
ex d being Function of T,S st [g,d] is Galois;
end;
:: Definition 3.1
definition
let S,T be non empty RelStr, d be Function of T,S;
attr d is lower_adjoint means
:: WAYBEL_1:def 12
ex g being Function of S,T st [g,d] is Galois;
end;
theorem :: WAYBEL_1:9
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:10
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:11
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:12
for S,T being non empty Poset,g being Function of S,T st g is
upper_adjoint holds g is infs-preserving;
registration
let S,T be non empty Poset;
cluster upper_adjoint -> infs-preserving for Function of S,T;
end;
:: Theorem 3.3 (second part)
theorem :: WAYBEL_1:13
for S,T being non empty Poset, d being Function of T,S st d is
lower_adjoint holds d is sups-preserving;
registration
let S,T be non empty Poset;
cluster lower_adjoint -> sups-preserving for Function of S,T;
end;
:: Theorem 3.4
theorem :: WAYBEL_1:14
for S,T being non empty Poset,g being Function of S,T st S is
complete & g is infs-preserving ex d being Function 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:15
for S,T being non empty Poset, d being Function of T,S st T is
complete & d is sups-preserving ex g being Function 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:16
for S,T being non empty Poset, g being Function of S,T st S is
complete holds (g is infs-preserving iff g is monotone & g is upper_adjoint);
:: Corollary 3.5 (ii)
theorem :: WAYBEL_1:17
for S,T being non empty Poset, d being Function of T,S st T is
complete holds d is sups-preserving iff d is monotone & d is lower_adjoint;
:: Theorem 3.6 (1) iff (2)
theorem :: WAYBEL_1:18
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:19
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:20
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:21
for S,T being non empty RelStr, g being Function of S,T, d being
Function of T,S st g = g*d*g holds g*d is idempotent;
:: Proposition 3.7 (1) implies (2)
theorem :: WAYBEL_1:22
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:23
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 (4) iff (1)
theorem :: WAYBEL_1:24
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:25
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:26
for S,T being non empty Poset,g being Function of S,T, d being
Function 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:27
for S,T being non empty Poset,g being Function of S,T, d being
Function 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 Function of L,L;
attr p is projection means
:: WAYBEL_1:def 13
p is idempotent monotone;
end;
registration
let L be non empty RelStr;
cluster id L -> projection;
end;
registration
let L be non empty RelStr;
cluster projection for Function of L,L;
end;
:: Definition 3.8 (ii)
definition
let L be non empty RelStr, c be Function of L,L;
attr c is closure means
:: WAYBEL_1:def 14
c is projection & id(L) <= c;
end;
registration
let L be non empty RelStr;
cluster closure -> projection for Function of L,L;
end;
registration
let L be non empty reflexive RelStr;
cluster closure for Function of L,L;
end;
registration
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 Function of L,L;
attr k is kernel means
:: WAYBEL_1:def 15
k is projection & k <= id(L);
end;
registration
let L be non empty RelStr;
cluster kernel -> projection for Function of L,L;
end;
registration
let L be non empty reflexive RelStr;
cluster kernel for Function of L,L;
end;
registration
let L be non empty reflexive RelStr;
cluster id L -> kernel;
end;
theorem :: WAYBEL_1:28
for L being non empty Poset, c being Function of L,L, X being
Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds inf X = c.(inf X
);
theorem :: WAYBEL_1:29
for L being non empty Poset, k being Function of L,L, X being
Subset of L st k is kernel & 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 Function of L1,L2;
func corestr(g) -> Function of L1,Image g equals
:: WAYBEL_1:def 16
(the carrier of Image g)|`g;
end;
theorem :: WAYBEL_1:30
for L1, L2 being non empty RelStr,g being Function of L1,L2
holds corestr g = g;
registration
let L1, L2 be non empty RelStr, g be Function of L1,L2;
cluster corestr g -> onto;
end;
theorem :: WAYBEL_1:31
for L1, L2 being non empty RelStr, g being Function of L1,L2 st
g is monotone holds corestr g is monotone;
definition
let L1, L2 be non empty RelStr, g be Function of L1,L2;
func inclusion(g) -> Function of Image g,L2 equals
:: WAYBEL_1:def 17
id Image g;
end;
registration
let L1, L2 be non empty RelStr, g be Function of L1,L2;
cluster inclusion g -> one-to-one monotone;
end;
theorem :: WAYBEL_1:32
for L being non empty RelStr, f being Function of L,L holds (
inclusion f)*(corestr f) = f;
::Theorem 3.10 (1) implies (2)
theorem :: WAYBEL_1:33
for L being non empty Poset, f being Function of L,L st f is
idempotent holds (corestr f)*(inclusion f) = id(Image f);
::Theorem 3.10 (1) implies (3)
theorem :: WAYBEL_1:34
for L being non empty Poset, f being Function of L,L st f is
projection ex T being non empty Poset, q being Function of L,T, i being
Function 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:35
for L being non empty Poset, f being Function of L,L st (ex T being
non empty Poset, q being Function of L,T, i being Function of T,L st q is
monotone & i is monotone & f = i*q & id(T) = q*i) holds f is projection;
::Theorem 3.10 (1_1) implies (2_1)
theorem :: WAYBEL_1:36
for L being non empty Poset, f being Function of L,L st f is
closure holds [inclusion f,corestr f] is Galois;
::Theorem 3.10 (2_1) implies (3_1)
theorem :: WAYBEL_1:37
for L being non empty Poset, f being Function of L,L st f is closure
ex S being non empty Poset, g being Function of S,L, d being Function of L,S st
[g,d] is Galois & f = g*d;
::Theorem 3.10 (3_1) implies (1_1)
theorem :: WAYBEL_1:38
for L being non empty Poset, f being Function of L,L st f is
monotone & ex S being non empty Poset, g being Function of S,L, d being
Function of L,S st [g,d] is Galois & f = g*d holds f is closure;
::Theorem 3.10 (1_2) implies (2_2)
theorem :: WAYBEL_1:39
for L being non empty Poset, f being Function of L,L st f is
kernel holds [corestr f,inclusion f] is Galois;
::Theorem 3.10 (2_2) implies (3_2)
theorem :: WAYBEL_1:40
for L being non empty Poset, f being Function of L,L st f is kernel ex
T being non empty Poset, g being Function of L,T, d being Function of T,L st [g
,d] is Galois & f = d*g;
::Theorem 3.10 (3_2) implies (1_2)
theorem :: WAYBEL_1:41
for L being non empty Poset, f being Function of L,L st f is monotone
& ex T being non empty Poset, g being Function of L,T, d being Function of T,L
st [g,d] is Galois & f = d*g holds f is kernel;
:: Lemma 3.11 (i) (part I)
theorem :: WAYBEL_1:42
for L being non empty Poset, p being Function of L,L st p is
projection 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:43
for L being non empty Poset, p being Function of L,L st p is
projection 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:44
for L being non empty Poset, p being Function of L,L st p is
projection 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:45
for L being non empty Poset, p being Function of L,L st p is
projection 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 Function of
subrelstr Lc,subrelstr Lc;
theorem :: WAYBEL_1:46
for L being non empty Poset, p being Function of L,L st p is
projection for Lk being non empty Subset of L st Lk = {k where k is Element of
L: p.k <= k} holds p|Lk is Function of subrelstr Lk,subrelstr Lk;
:: Lemma 3.11 (i) (part IIIa)
theorem :: WAYBEL_1:47
for L being non empty Poset, p being Function of L,L st p is
projection for Lc being non empty Subset of L st Lc = {c where c is Element of
L: c <= p.c} for pc being Function of subrelstr Lc,subrelstr Lc st pc = p|Lc
holds pc is closure;
:: Lemma 3.11 (i) (part IIIb)
theorem :: WAYBEL_1:48
for L being non empty Poset, p being Function of L,L st p is
projection for Lk being non empty Subset of L st Lk = {k where k is Element of
L: p.k <= k} for pk being Function of subrelstr Lk,subrelstr Lk st pk = p|Lk
holds pk is kernel;
:: Lemma 3.11 (ii) (part I)
theorem :: WAYBEL_1:49
for L being non empty Poset, p being Function 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:50
for L being non empty Poset, p being Function 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:51
for L being non empty Poset, p being Function of L,L st p is
projection 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:52
for L being non empty Poset, p being Function of L,L st p is
projection 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:53
for L being non empty Poset, p being Function of L,L holds (p is
closure implies Image p is infs-inheriting) & (p is kernel implies Image p is
sups-inheriting);
:: Proposition 3.12 (ii)
theorem :: WAYBEL_1:54
for L being complete non empty Poset, p being Function of L,L st p
is projection holds Image p is complete;
:: Proposition 3.12 (iii)
theorem :: WAYBEL_1:55
for L being non empty Poset, c being Function of L,L st c is closure
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:56
for L being non empty Poset, k being Function of L,L st k is kernel
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:57
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:58
for L being complete non empty Poset holds (IdsMap L)*(SupMap L) is
closure & Image ((IdsMap L)*(SupMap L)),L are_isomorphic;
definition
let S be non empty RelStr;
let x be Element of S;
func x "/\" -> Function of S,S means
:: WAYBEL_1:def 18
for s being Element of S holds it.s = x"/\"s;
end;
theorem :: WAYBEL_1:59
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:60
for S being Semilattice, x be Element of S holds x "/\" is monotone;
registration
let S be Semilattice, x be Element of S;
cluster x "/\" -> monotone;
end;
theorem :: WAYBEL_1:61
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:62
for S being Semilattice holds (for x being Element of S holds x
"/\" is lower_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:63
for S being Semilattice st for x being Element of S holds x "/\"
is lower_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:64
for S being complete non empty Poset holds (for x being Element of S
holds x "/\" is lower_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:65
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 "/\" is lower_adjoint;
end;
registration
cluster Heyting -> with_infima with_suprema reflexive transitive
antisymmetric for non empty RelStr;
end;
definition
let H be non empty RelStr, a be Element of H;
assume
H is Heyting;
func a => -> Function of H,H means
:: WAYBEL_1:def 20
[it,a "/\"] is Galois;
end;
theorem :: WAYBEL_1:66
for H being non empty RelStr st H is Heyting holds H is distributive;
registration
cluster Heyting -> distributive for 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:67
for H being non empty RelStr st H is Heyting for x,a,y being
Element of H holds x >= a "/\" y iff a => x >= y;
theorem :: WAYBEL_1:68
for H being non empty RelStr st H is Heyting holds H is upper-bounded;
registration
cluster Heyting -> upper-bounded for non empty RelStr;
end;
theorem :: WAYBEL_1:69
for H being non empty RelStr st H is Heyting for a,b being
Element of H holds Top H = a => b iff a <= b;
theorem :: WAYBEL_1:70
for H being non empty RelStr st H is Heyting for a being Element of H
holds Top H = a => a;
theorem :: WAYBEL_1:71
for H being non empty RelStr st H is Heyting for a,b being Element of
H st Top H = a => b & Top H = b => a holds a = b;
theorem :: WAYBEL_1:72
for H being non empty RelStr st H is Heyting for a,b being
Element of H holds b <= (a => b);
theorem :: WAYBEL_1:73
for H being non empty RelStr st H is Heyting for a being Element of H
holds Top H = a => Top H;
theorem :: WAYBEL_1:74
for H being non empty RelStr st H is Heyting for b being Element of H
holds b = (Top H) => b;
theorem :: WAYBEL_1:75
for H being non empty RelStr st H is Heyting for a,b,c being
Element of H st a <= b holds (b => c) <= (a => c);
theorem :: WAYBEL_1:76
for H being non empty RelStr st H is Heyting for a,b,c being Element
of H st b <= c holds (a => b) <= (a => c);
theorem :: WAYBEL_1:77
for H being non empty RelStr st H is Heyting for a,b being
Element of H holds a"/\"(a => b) = a"/\"b;
theorem :: WAYBEL_1:78
for H being non empty RelStr st H is Heyting 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:79
for H being non empty RelStr st H is Heyting & 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:80
for H being non empty RelStr st H is Heyting & H is
lower-bounded holds 'not' Bottom H = Top H & 'not' Top H = Bottom H;
:: Exercise 3.18 (i)
theorem :: WAYBEL_1:81
for H being non empty lower-bounded RelStr st H is Heyting for a,b
being Element of H holds 'not' a >= b iff 'not' b >= a;
:: Exercise 3.18 (ii)
theorem :: WAYBEL_1:82
for H being non empty lower-bounded RelStr st H is Heyting for a
,b being Element of H holds 'not' a >= b iff a "/\" b = Bottom H;
theorem :: WAYBEL_1:83
for H being non empty lower-bounded RelStr st H is Heyting for a,b
being Element of H st a <= b holds 'not' b <= 'not' a;
theorem :: WAYBEL_1:84
for H being non empty lower-bounded RelStr st H is Heyting for a,b
being Element of H holds 'not' (a"\/"b) = 'not' a"/\"'not' b;
theorem :: WAYBEL_1:85
for H being non empty lower-bounded RelStr st H is Heyting 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;
registration
let X be set;
cluster BoolePoset X -> complemented;
end;
:: Exercise 3.19
theorem :: WAYBEL_1:86
for L being bounded LATTICE st L is Heyting & 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:87
for L being bounded LATTICE holds L is distributive complemented
iff L is Heyting & 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;
end;
registration
cluster Boolean -> reflexive transitive antisymmetric with_infima
with_suprema bounded distributive complemented for non empty RelStr;
end;
registration
cluster reflexive transitive antisymmetric with_infima with_suprema bounded
distributive complemented -> Boolean for non empty RelStr;
end;
registration
cluster Boolean -> Heyting for non empty RelStr;
end;
registration
cluster strict Boolean non empty for LATTICE;
end;
registration
cluster strict Heyting non empty for LATTICE;
end;