:: Galois Connections
:: by Czes\law Byli\'nski
::
:: Received September 25, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users


definition
let L1, L2 be non empty 1-sorted ;
let f be Function of L1,L2;
:: original: one-to-one
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;
compatibility
( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds
x = y )
proof end;
end;

:: deftheorem defines one-to-one WAYBEL_1:def 1 :
for L1, L2 being non empty 1-sorted
for f being Function of L1,L2 holds
( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds
x = y );

definition
let L1, L2 be non empty RelStr ;
let 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;
compatibility
( f is monotone iff for x, y being Element of L1 st x <= y holds
f . x <= f . y ) ;
end;

:: deftheorem defines monotone WAYBEL_1:def 2 :
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is monotone iff for x, y being Element of L1 st x <= y holds
f . x <= f . y );

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

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

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

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

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

:: deftheorem Def3 defines distributive WAYBEL_1:def 3 :
for L being non empty RelStr holds
( L is distributive iff for x, y, z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) );

theorem Th5: :: 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) )
proof end;

registration
let X be set ;
cluster BoolePoset X -> distributive ;
coherence
BoolePoset X is distributive
proof end;
end;

definition
let S be non empty RelStr ;
let 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;

:: deftheorem defines ex_min_of WAYBEL_1:def 4 :
for S being non empty RelStr
for X being set holds
( ex_min_of X,S iff ( ex_inf_of X,S & "/\" (X,S) in X ) );

:: deftheorem defines ex_max_of WAYBEL_1:def 5 :
for S being non empty RelStr
for X being set holds
( ex_max_of X,S iff ( ex_sup_of X,S & "\/" (X,S) in X ) );

notation
let S be non empty RelStr ;
let 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 ;
let s be Element of S;
let 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;

:: deftheorem defines is_minimum_of WAYBEL_1:def 6 :
for S being non empty RelStr
for s being Element of S
for X being set holds
( s is_minimum_of X iff ( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X ) );

:: deftheorem defines is_maximum_of WAYBEL_1:def 7 :
for S being non empty RelStr
for s being Element of S
for X being set holds
( s is_maximum_of X iff ( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X ) );

registration
let L be RelStr ;
cluster id L -> isomorphic ;
coherence
id L is isomorphic
proof end;
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
for L1 being RelStr ex f being Function of L1,L1 st f is isomorphic
proof end;
end;

:: deftheorem defines are_isomorphic WAYBEL_1:def 8 :
for L1, L2 being RelStr holds
( L1,L2 are_isomorphic iff ex f being Function of L1,L2 st f is isomorphic );

theorem :: WAYBEL_1:6
for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds
L2,L1 are_isomorphic
proof end;

theorem :: WAYBEL_1:7
for L1, L2, L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds
L1,L3 are_isomorphic
proof end;

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

:: deftheorem Def9 defines Connection WAYBEL_1:def 9 :
for S, T being RelStr
for b3 being set holds
( b3 is Connection of S,T iff ex g being Function of S,T ex d being Function of T,S st b3 = [g,d] );

definition
let S, T be RelStr ;
let g be Function of S,T;
let d be Function of T,S;
:: original: [
redefine func [g,d] -> Connection of S,T;
coherence
[g,d] is Connection of S,T by Def9;
end;

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

:: deftheorem defines Galois WAYBEL_1:def 10 :
for S, T being non empty RelStr
for gc being Connection of S,T holds
( gc is Galois iff ex g being Function of S,T ex d being Function of T,S st
( gc = [g,d] & g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) );

theorem Th8: :: WAYBEL_1:8
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )
proof end;

:: Definition 3.1
definition
let S, T be non empty RelStr ;
let 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;

:: deftheorem defines upper_adjoint WAYBEL_1:def 11 :
for S, T being non empty RelStr
for g being Function of S,T holds
( g is upper_adjoint iff ex d being Function of T,S st [g,d] is Galois );

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

:: deftheorem Def12 defines lower_adjoint WAYBEL_1:def 12 :
for S, T being non empty RelStr
for d being Function of T,S holds
( d is lower_adjoint iff ex g being Function of S,T st [g,d] is Galois );

theorem :: WAYBEL_1:9
for S, T being non empty Poset
for g being Function of S,T
for 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 Th10: :: WAYBEL_1:10
for S, T being non empty Poset
for g being Function of S,T
for 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) ) ) )
proof end;

:: Theorem 3.2 (1) iff (3)
theorem Th11: :: WAYBEL_1:11
for S, T being non empty Poset
for g being Function of S,T
for 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) ) ) )
proof end;

:: Theorem 3.3 (first part)
theorem Th12: :: WAYBEL_1:12
for S, T being non empty Poset
for g being Function of S,T st g is upper_adjoint holds
g is infs-preserving
proof end;

registration
let S, T be non empty Poset;
cluster Function-like quasi_total upper_adjoint -> infs-preserving for M3( bool [: the carrier of S, the carrier of T:]);
coherence
for b1 being Function of S,T st b1 is upper_adjoint holds
b1 is infs-preserving by Th12;
end;

:: Theorem 3.3 (second part)
theorem Th13: :: WAYBEL_1:13
for S, T being non empty Poset
for d being Function of T,S st d is lower_adjoint holds
d is sups-preserving
proof end;

registration
let S, T be non empty Poset;
cluster Function-like quasi_total lower_adjoint -> sups-preserving for M3( bool [: the carrier of S, the carrier of T:]);
coherence
for b1 being Function of S,T st b1 is lower_adjoint holds
b1 is sups-preserving by Th13;
end;

:: Theorem 3.4
theorem Th14: :: WAYBEL_1:14
for S, T being non empty Poset
for g being Function of S,T st S is complete & g is infs-preserving holds
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) ) )
proof end;

:: Theorem 3.4 (dual)
theorem Th15: :: WAYBEL_1:15
for S, T being non empty Poset
for d being Function of T,S st T is complete & d is sups-preserving holds
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) ) )
proof end;

:: Corollary 3.5 (i)
theorem :: WAYBEL_1:16
for S, T being non empty Poset
for g being Function of S,T st S is complete holds
( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) )
proof end;

:: Corollary 3.5 (ii)
theorem Th17: :: WAYBEL_1:17
for S, T being non empty Poset
for d being Function of T,S st T is complete holds
( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) )
proof end;

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

:: Theorem 3.6 (2) implies (1)
theorem Th19: :: WAYBEL_1:19
for S, T being non empty Poset
for g being Function of S,T
for 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
proof end;

:: Theorem 3.6 (2) implies (3)
theorem Th20: :: WAYBEL_1:20
for S, T being non empty Poset
for g being Function of S,T
for 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 )
proof end;

:: Theorem 3.6 (3) implies (4)
theorem Th21: :: WAYBEL_1:21
for S, T being non empty RelStr
for g being Function of S,T
for d being Function of T,S st g = (g * d) * g holds
g * d is idempotent
proof end;

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

:: Proposition 3.7 (2) implies (3)
theorem Th23: :: WAYBEL_1:23
for S, T being non empty Poset
for g being Function of S,T
for 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
proof end;

:: Proposition 3.7 (4) iff (1)
theorem :: WAYBEL_1:24
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is onto iff d is V13() )
proof end;

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

:: Proposition 3.7 (2*) implies (3*)
theorem Th26: :: WAYBEL_1:26
for S, T being non empty Poset
for g being Function of S,T
for 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
proof end;

:: Proposition 3.7 (1*) iff (4*)
theorem :: WAYBEL_1:27
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is V13() iff d is onto )
proof end;

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

:: deftheorem Def13 defines projection WAYBEL_1:def 13 :
for L being non empty RelStr
for p being Function of L,L holds
( p is projection iff ( p is idempotent & p is monotone ) );

registration
let L be non empty RelStr ;
cluster id L -> projection ;
coherence
id L is projection by YELLOW_2:21;
end;

registration
let L be non empty RelStr ;
cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total projection for M3( bool [: the carrier of L, the carrier of L:]);
existence
ex b1 being Function of L,L st b1 is projection
proof end;
end;

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

:: deftheorem defines closure WAYBEL_1:def 14 :
for L being non empty RelStr
for c being Function of L,L holds
( c is closure iff ( c is projection & id L <= c ) );

registration
let L be non empty RelStr ;
cluster Function-like quasi_total closure -> projection for M3( bool [: the carrier of L, the carrier of L:]);
coherence
for b1 being Function of L,L st b1 is closure holds
b1 is projection ;
end;

Lm1: for L1, L2 being non empty RelStr
for f being Function of L1,L2 st L2 is reflexive holds
f <= f
proof end;

registration
let L be non empty reflexive RelStr ;
cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total closure for M3( bool [: the carrier of L, the carrier of L:]);
existence
ex b1 being Function of L,L st b1 is closure
proof end;
end;

registration
let L be non empty reflexive RelStr ;
cluster id L -> closure ;
coherence
id L is closure by Lm1;
end;

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

:: deftheorem defines kernel WAYBEL_1:def 15 :
for L being non empty RelStr
for k being Function of L,L holds
( k is kernel iff ( k is projection & k <= id L ) );

registration
let L be non empty RelStr ;
cluster Function-like quasi_total kernel -> projection for M3( bool [: the carrier of L, the carrier of L:]);
coherence
for b1 being Function of L,L st b1 is kernel holds
b1 is projection ;
end;

registration
let L be non empty reflexive RelStr ;
cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total kernel for M3( bool [: the carrier of L, the carrier of L:]);
existence
ex b1 being Function of L,L st b1 is kernel
proof end;
end;

registration
let L be non empty reflexive RelStr ;
cluster id L -> kernel ;
coherence
id L is kernel by Lm1;
end;

Lm2: for L being non empty 1-sorted
for p being Function of L,L st p is idempotent holds
for x being set st x in rng p holds
p . x = x
proof end;

theorem Th28: :: WAYBEL_1:28
for L being non empty Poset
for c being Function of L,L
for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)
proof end;

theorem Th29: :: WAYBEL_1:29
for L being non empty Poset
for k being Function of L,L
for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)
proof end;

definition
let L1, L2 be non empty RelStr ;
let 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;
coherence
the carrier of (Image g) |` g is Function of L1,(Image g)
proof end;
end;

:: deftheorem defines corestr WAYBEL_1:def 16 :
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g = the carrier of (Image g) |` g;

theorem Th30: :: WAYBEL_1:30
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g = g
proof end;

Lm3: for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g is onto
proof end;

registration
let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;
cluster corestr g -> onto ;
coherence
corestr g is onto by Lm3;
end;

theorem Th31: :: WAYBEL_1:31
for L1, L2 being non empty RelStr
for g being Function of L1,L2 st g is monotone holds
corestr g is monotone
proof end;

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

:: deftheorem defines inclusion WAYBEL_1:def 17 :
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g = id (Image g);

Lm4: for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g is monotone
by YELLOW_0:59;

registration
let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;
cluster inclusion g -> V13() monotone ;
coherence
( inclusion g is one-to-one & inclusion g is monotone ) by Lm4;
end;

theorem Th32: :: WAYBEL_1:32
for L being non empty RelStr
for f being Function of L,L holds (inclusion f) * (corestr f) = f
proof end;

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

::Theorem 3.10 (1) implies (3)
theorem :: WAYBEL_1:34
for L being non empty Poset
for f being Function of L,L st f is projection holds
ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )
proof end;

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

::Theorem 3.10 (1_1) implies (2_1)
theorem Th36: :: WAYBEL_1:36
for L being non empty Poset
for f being Function of L,L st f is closure holds
[(inclusion f),(corestr f)] is Galois
proof end;

::Theorem 3.10 (2_1) implies (3_1)
theorem :: WAYBEL_1:37
for L being non empty Poset
for f being Function of L,L st f is closure holds
ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d )
proof end;

::Theorem 3.10 (3_1) implies (1_1)
theorem Th38: :: WAYBEL_1:38
for L being non empty Poset
for f being Function of L,L st f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d ) holds
f is closure
proof end;

::Theorem 3.10 (1_2) implies (2_2)
theorem Th39: :: WAYBEL_1:39
for L being non empty Poset
for f being Function of L,L st f is kernel holds
[(corestr f),(inclusion f)] is Galois
proof end;

::Theorem 3.10 (2_2) implies (3_2)
theorem :: WAYBEL_1:40
for L being non empty Poset
for f being Function of L,L st f is kernel holds
ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
proof end;

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

:: Lemma 3.11 (i) (part I)
theorem Th42: :: WAYBEL_1:42
for L being non empty Poset
for 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 }
proof end;

theorem Th43: :: WAYBEL_1:43
for L being non empty Poset
for 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 )
proof end;

:: Lemma 3.11 (i) (part II)
theorem Th44: :: WAYBEL_1:44
for L being non empty Poset
for 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 )
proof end;

theorem Th45: :: WAYBEL_1:45
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc, 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)
proof end;

theorem :: WAYBEL_1:46
for L being non empty Poset
for p being Function of L,L st p is projection holds
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)
proof end;

:: Lemma 3.11 (i) (part IIIa)
theorem Th47: :: WAYBEL_1:47
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure
proof end;

:: Lemma 3.11 (i) (part IIIb)
theorem :: WAYBEL_1:48
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
proof end;

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

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

:: Lemma 3.11 (iii) (part I)
theorem :: WAYBEL_1:51
for L being non empty Poset
for p being Function of L,L st p is projection holds
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 ) ) )
proof end;

:: Lemma 3.11 (iii) (part II)
theorem :: WAYBEL_1:52
for L being non empty Poset
for p being Function of L,L st p is projection holds
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 ) ) )
proof end;

:: Proposition 3.12 (i)
theorem Th53: :: WAYBEL_1:53
for L being non empty Poset
for 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 ) )
proof end;

:: Proposition 3.12 (ii)
theorem :: WAYBEL_1:54
for L being non empty complete Poset
for p being Function of L,L st p is projection holds
Image p is complete
proof end;

:: Proposition 3.12 (iii)
theorem :: WAYBEL_1:55
for L being non empty Poset
for 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)) ) ) )
proof end;

:: Proposition 3.12 (iv)
theorem :: WAYBEL_1:56
for L being non empty Poset
for 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)) ) ) )
proof end;

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

:: Proposition 3.15 (ii)
theorem :: WAYBEL_1:58
for L being non empty complete Poset holds
( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic )
proof end;

definition
let S be non empty RelStr ;
let x be Element of S;
func x "/\" -> Function of S,S means :Def18: :: WAYBEL_1:def 18
 for s being Element of S holds it . s = x "/\" s;
existence
ex b1 being Function of S,S st
for s being Element of S holds b1 . s = x "/\" s
proof end;
uniqueness
for b1, b2 being Function of S,S st ( for s being Element of S holds b1 . s = x "/\" s ) & ( for s being Element of S holds b2 . s = x "/\" s ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines "/\" WAYBEL_1:def 18 :
for S being non empty RelStr
for x being Element of S
for b3 being Function of S,S holds
( b3 = x "/\" iff for s being Element of S holds b3 . s = x "/\" s );

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

theorem Th60: :: WAYBEL_1:60
for S being Semilattice
for x being Element of S holds x "/\" is monotone
proof end;

registration
let S be Semilattice;
let x be Element of S;
cluster x "/\" -> monotone ;
coherence
x "/\" is monotone by Th60;
end;

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

:: Lemma 3.16 (1) iff (2)
theorem Th62: :: 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 )
proof end;

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

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

:: Lemma 3.16 (3) implies (D)
theorem Th65: :: WAYBEL_1:65
for S being LATTICE st ( for X being Subset of S st ex_sup_of X,S holds
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
proof end;

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;

:: deftheorem defines Heyting WAYBEL_1:def 19 :
for H being non empty RelStr holds
( H is Heyting iff ( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) ) );

registration
cluster non empty Heyting -> non empty reflexive transitive antisymmetric with_suprema with_infima for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Heyting holds
( b1 is with_infima & b1 is with_suprema & b1 is reflexive & b1 is transitive & b1 is antisymmetric ) ;
end;

definition
let H be non empty RelStr ;
let a be Element of H;
assume A1: H is Heyting ;
func a => -> Function of H,H means :Def20: :: WAYBEL_1:def 20
[it,(a "/\")] is Galois ;
existence
ex b1 being Function of H,H st [b1,(a "/\")] is Galois by A1, Def12;
uniqueness
for b1, b2 being Function of H,H st [b1,(a "/\")] is Galois & [b2,(a "/\")] is Galois holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines => WAYBEL_1:def 20 :
for H being non empty RelStr
for a being Element of H st H is Heyting holds
for b3 being Function of H,H holds
( b3 = a => iff [b3,(a "/\")] is Galois );

theorem Th66: :: WAYBEL_1:66
for H being non empty RelStr st H is Heyting holds
H is distributive
proof end;

registration
cluster non empty Heyting -> non empty distributive for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Heyting holds
b1 is distributive by Th66;
end;

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

:: deftheorem defines => WAYBEL_1:def 21 :
for H being non empty RelStr
for a, y being Element of H holds a => y = (a =>) . y;

theorem Th67: :: WAYBEL_1:67
for H being non empty RelStr st H is Heyting holds
for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y )
proof end;

theorem Th68: :: WAYBEL_1:68
for H being non empty RelStr st H is Heyting holds
H is upper-bounded
proof end;

registration
cluster non empty Heyting -> non empty upper-bounded for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Heyting holds
b1 is upper-bounded by Th68;
end;

theorem Th69: :: WAYBEL_1:69
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds
( Top H = a => b iff a <= b )
proof end;

theorem :: WAYBEL_1:70
for H being non empty RelStr st H is Heyting holds
for a being Element of H holds Top H = a => a
proof end;

theorem :: WAYBEL_1:71
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H st Top H = a => b & Top H = b => a holds
a = b
proof end;

theorem Th72: :: WAYBEL_1:72
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds b <= a => b
proof end;

theorem :: WAYBEL_1:73
for H being non empty RelStr st H is Heyting holds
for a being Element of H holds Top H = a => (Top H)
proof end;

theorem :: WAYBEL_1:74
for H being non empty RelStr st H is Heyting holds
for b being Element of H holds b = (Top H) => b
proof end;

Lm5: for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds a "/\" (a => b) <= b
proof end;

theorem Th75: :: WAYBEL_1:75
for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H st a <= b holds
b => c <= a => c
proof end;

theorem :: WAYBEL_1:76
for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H st b <= c holds
a => b <= a => c
proof end;

theorem Th77: :: WAYBEL_1:77
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds a "/\" (a => b) = a "/\" b
proof end;

theorem Th78: :: WAYBEL_1:78
for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c)
proof end;

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

:: deftheorem defines 'not' WAYBEL_1:def 22 :
for H being non empty RelStr
for a being Element of H holds 'not' a = a => (Bottom H);

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

theorem Th80: :: 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 )
proof end;

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

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

theorem :: WAYBEL_1:83
for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H st a <= b holds
'not' b <= 'not' a
proof end;

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

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

definition
let L be non empty RelStr ;
let 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;

:: deftheorem defines is_a_complement_of WAYBEL_1:def 23 :
for L being non empty RelStr
for x, y being Element of L holds
( y is_a_complement_of x iff ( x "\/" y = Top L & x "/\" y = Bottom L ) );

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;

:: deftheorem defines complemented WAYBEL_1:def 24 :
for L being non empty RelStr holds
( L is complemented iff for x being Element of L ex y being Element of L st y is_a_complement_of x );

registration
let X be set ;
cluster BoolePoset X -> complemented ;
coherence
BoolePoset X is complemented
proof end;
end;

Lm6: for L being bounded LATTICE st L is distributive & L is complemented holds
for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
proof end;

Lm7: for L being bounded LATTICE st ( for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) holds
( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )
proof end;

:: Exercise 3.19
theorem Th86: :: WAYBEL_1:86
for L being bounded LATTICE st L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) holds
for x being Element of L holds 'not' x is_a_complement_of x
proof end;

:: Exercise 3.19 (1) iff (2)
theorem Th87: :: WAYBEL_1:87
for L being bounded LATTICE holds
( L is distributive & L is complemented iff ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) )
proof end;

:: 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 & B is distributive & B is complemented );
end;

:: deftheorem defines Boolean WAYBEL_1:def 25 :
for B being non empty RelStr holds
( B is Boolean iff ( B is LATTICE & B is bounded & B is distributive & B is complemented ) );

registration
cluster non empty Boolean -> non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Boolean holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_infima & b1 is with_suprema & b1 is bounded & b1 is distributive & b1 is complemented ) ;
end;

registration
cluster non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented -> non empty Boolean for RelStr ;
coherence
for b1 being non empty RelStr st b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_infima & b1 is with_suprema & b1 is bounded & b1 is distributive & b1 is complemented holds
b1 is Boolean ;
end;

registration
cluster non empty Boolean -> non empty Heyting for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Boolean holds
b1 is Heyting by Th87;
end;

registration
cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Boolean for RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & b1 is Boolean & not b1 is empty )
proof end;
end;

registration
cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Heyting for RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & b1 is Heyting & not b1 is empty )
proof end;
end;