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


begin

definition
let L1, L2 be non empty 1-sorted ;
let f be Function of L1,L2;
:: original:one-to-one
redefine attrf 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 )
proofend;
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 :Def2: :: 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 )
proofend;
end;

:: deftheorem Def2 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
proofend;

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
proofend;

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 ) &amp; ( L is with_suprema &amp; L is reflexive &amp; L is transitive implies (Bottom L) "\/" x = x ) )
proofend;

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 &amp; L is transitive &amp; L is reflexive implies (Top L) "/\" x = x ) &amp; ( L is with_suprema implies (Top L) "\/" x = Top L ) )
proofend;

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

registration
let X be set ;
cluster BoolePoset X ->  distributive ;
coherence
 BoolePoset X is distributive
proofend;
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 &amp; "/\" (X,S) in X );
pred ex_max_of X,S means :Def5: :: WAYBEL_1:def 5
( ex_sup_of X,S &amp; "\/" (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 &amp; "/\" (X,S) in X ) );

:: deftheorem Def5 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 &amp; "\/" (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 ;
preds is_minimum_of X means :Def6: :: WAYBEL_1:def 6
( ex_inf_of X,S &amp; s = "/\" (X,S) &amp; "/\" (X,S) in X );
preds is_maximum_of X means :Def7: :: WAYBEL_1:def 7
( ex_sup_of X,S &amp; s = "\/" (X,S) &amp; "\/" (X,S) in X );
end;

:: deftheorem Def6 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 &amp; s = "/\" (X,S) &amp; "/\" (X,S) in X ) );

:: deftheorem Def7 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 &amp; s = "\/" (X,S) &amp; "\/" (X,S) in X ) );

registration
let L be RelStr ;
cluster id L ->  isomorphic ;
coherence
 id L is isomorphic
proofend;
end;

definition
let L1, L2 be RelStr ;
predL1,L2 are_isomorphic  means :Def8: :: 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
proofend;
end;

:: deftheorem Def8 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
proofend;

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

begin

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]
proofend;
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;
attrgc is Galois  means :Def10: :: WAYBEL_1:def 10
 ex g being Function of S,T ex d being Function of T,S st
( gc = [g,d] &amp; g is monotone &amp; d is monotone &amp; ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) );
end;

:: deftheorem Def10 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] &amp; g is monotone &amp; d is monotone &amp; ( 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 &amp; d is monotone &amp; ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )
proofend;

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

:: deftheorem Def11 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;
attrd 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 Th9: :: 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 &amp; d is lower_adjoint )
proofend;

:: 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 &amp; ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )
proofend;

:: 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 &amp; ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
proofend;

:: 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
proofend;

registration
let S, T be non empty Poset;
cluster Function-like quasi_total upper_adjoint  ->  infs-preserving for M2( 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
proofend;

registration
let S, T be non empty Poset;
cluster Function-like quasi_total lower_adjoint  ->  sups-preserving for M2( 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 &amp; g is infs-preserving holds
ex d being Function of T,S st
( [g,d] is Galois &amp; ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
proofend;

:: 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 &amp; d is sups-preserving holds
ex g being Function of S,T st
( [g,d] is Galois &amp; ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
proofend;

:: 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 &amp; g is upper_adjoint ) )
proofend;

:: 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 &amp; d is lower_adjoint ) )
proofend;

:: 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 &amp; id T <= g * d )
proofend;

:: 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 &amp; d is monotone &amp; d * g <= id S &amp; id T <= g * d holds
[g,d] is Galois
proofend;

:: 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 &amp; d is monotone &amp; d * g <= id S &amp; id T <= g * d holds
( d = (d * g) * d &amp; g = (g * d) * g )
proofend;

:: 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
proofend;

:: 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 &amp; g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}
proofend;

:: 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
proofend;

:: 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() )
proofend;

:: 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 &amp; d is onto holds
for s being Element of S holds g . s is_maximum_of d " {s}
proofend;

:: 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
proofend;

:: 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 )
proofend;

:: Definition 3.8 (i)
definition
let L be non empty RelStr ;
let p be Function of L,L;
attrp is projection  means :Def13: :: WAYBEL_1:def 13
( p is idempotent &amp; 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 &amp; p is monotone ) );

registration
let L be non empty RelStr ;
cluster id L ->  projection ;
coherence
 id L is projection
proofend;
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 M2( bool [: the carrier of L, the carrier of L:]);
existence
 ex b1 being Function of L,L st b1 is projection
proofend;
end;

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

:: deftheorem Def14 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 &amp; id L <= c ) );

registration
let L be non empty RelStr ;
cluster Function-like quasi_total closure  ->  projection for M2( 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 by Def14;
end;

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

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 M2( bool [: the carrier of L, the carrier of L:]);
existence
 ex b1 being Function of L,L st b1 is closure
proofend;
end;

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

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

:: deftheorem Def15 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 &amp; k <= id L ) );

registration
let L be non empty RelStr ;
cluster Function-like quasi_total kernel  ->  projection for M2( 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 by Def15;
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 M2( bool [: the carrier of L, the carrier of L:]);
existence
 ex b1 being Function of L,L st b1 is kernel
proofend;
end;

registration
let L be non empty reflexive RelStr ;
cluster id L ->  kernel ;
coherence
 id L is kernel
proofend;
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
proofend;

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 &amp; ex_inf_of X,L &amp; X c= rng c holds
inf X = c . (inf X)
proofend;

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 &amp; ex_sup_of X,L &amp; X c= rng k holds
sup X = k . (sup X)
proofend;

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)
proofend;
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
proofend;

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

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
proofend;

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
proofend;
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
proofend;

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 &amp; 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
proofend;

::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)
proofend;

::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 &amp; q is onto &amp; i is monotone &amp; i is V13() &amp; f = i * q &amp; id T = q * i )
proofend;

::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 &amp; i is monotone &amp; f = i * q &amp; id T = q * i ) holds
f is projection
proofend;

::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
proofend;

::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 &amp; f = g * d )
proofend;

::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 &amp; 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 &amp; f = g * d ) holds
f is closure
proofend;

::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
proofend;

::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 &amp; f = d * g )
proofend;

::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 &amp; 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 &amp; f = d * g ) holds
f is kernel
proofend;

:: 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  }
proofend;

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 &amp;  {  k where k is Element of L : p . k <= k  }  is non empty Subset of L )
proofend;

:: 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 &amp; rng (p |  {  k where k is Element of L : p . k <= k  }  ) = rng p )
proofend;

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)
proofend;

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)
proofend;

:: 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
proofend;

:: 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
proofend;

:: 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
proofend;

:: 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
proofend;

:: 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 &amp; Image p is infs-inheriting ) ) &amp; ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting &amp; Image p is filtered-infs-inheriting ) ) )
proofend;

:: 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 &amp; Image p is sups-inheriting ) ) &amp; ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting &amp; Image p is directed-sups-inheriting ) ) )
proofend;

:: 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 ) &amp; ( p is kernel implies Image p is sups-inheriting ) )
proofend;

:: 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
proofend;

:: 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 &amp; ( for X being Subset of L st X c= the carrier of (Image c) &amp; ex_sup_of X,L holds
( ex_sup_of X, Image c &amp; "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) )
proofend;

:: 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 &amp; ( for X being Subset of L st X c= the carrier of (Image k) &amp; ex_inf_of X,L holds
( ex_inf_of X, Image k &amp; "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) )
proofend;

begin

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

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

definition
let S be non empty RelStr ;
let x be Element of S;
funcx "/\"  ->  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
proofend;
uniqueness
 for b1, b2 being Function of S,S st ( for s being Element of S holds b1 . s = x "/\" s ) &amp; ( for s being Element of S holds b2 . s = x "/\" s ) holds
b1 = b2
proofend;
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)
proofend;

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

registration
let S be Semilattice;
let x be Element of S;
clusterx "/\"  ->  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  }
proofend;

:: 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 )
proofend;

:: 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)
proofend;

:: 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) )
proofend;

:: 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
proofend;

definition
let H be non empty RelStr ;
attrH is Heyting  means :Def19: :: WAYBEL_1:def 19
( H is LATTICE &amp; ( for x being Element of H holds x "/\" is lower_adjoint ) );
end;

:: deftheorem Def19 defines Heyting WAYBEL_1:def_19_:_
 for H being non empty RelStr holds
( H is Heyting iff ( H is LATTICE &amp; ( 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 &amp; b1 is with_suprema &amp; b1 is reflexive &amp; b1 is transitive &amp; b1 is antisymmetric ) by Def19;
end;

definition
let H be non empty RelStr ;
let a be Element of H;
assume A1: H is Heyting ;
funca =>  ->  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
proofend;
uniqueness
 for b1, b2 being Function of H,H st [b1,(a "/\")] is Galois &amp; [b2,(a "/\")] is Galois holds
b1 = b2
proofend;
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
proofend;

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;
funca => 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 )
proofend;

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

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 )
proofend;

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
proofend;

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 &amp; Top H = b => a holds
a = b
proofend;

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
proofend;

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)
proofend;

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
proofend;

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

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
proofend;

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
proofend;

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
proofend;

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)
proofend;

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 &amp; 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  }
proofend;

theorem Th80: :: WAYBEL_1:80
for H being non empty RelStr st H is Heyting &amp; H is lower-bounded holds
( 'not' (Bottom H) = Top H &amp; 'not' (Top H) = Bottom H )
proofend;

:: 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 )
proofend;

:: 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 )
proofend;

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
proofend;

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)
proofend;

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

:: deftheorem Def23 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 &amp; x "/\" y = Bottom L ) );

definition
let L be non empty RelStr ;
attrL is complemented  means :Def24: :: 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 Def24 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
proofend;
end;

Lm6:  for L being bounded LATTICE st L is distributive &amp; 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 &amp; y <= (y "/\" x) "\/" x9 )
proofend;

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 &amp; y <= (y "/\" x) "\/" x9 ) ) holds
( L is Heyting &amp; ( for x being Element of L holds 'not' ('not' x) = x ) )
proofend;

:: Exercise 3.19
theorem Th86: :: WAYBEL_1:86
for L being bounded LATTICE st L is Heyting &amp; ( 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
proofend;

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

:: Definition 3.20
definition
let B be non empty RelStr ;
attrB is Boolean  means :Def25: :: WAYBEL_1:def 25
( B is LATTICE &amp; B is bounded &amp; B is distributive &amp; B is complemented );
end;

:: deftheorem Def25 defines Boolean WAYBEL_1:def_25_:_
 for B being non empty RelStr holds
( B is Boolean iff ( B is LATTICE &amp; B is bounded &amp; B is distributive &amp; 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 &amp; b1 is transitive &amp; b1 is antisymmetric &amp; b1 is with_infima &amp; b1 is with_suprema &amp; b1 is bounded &amp; b1 is distributive &amp; b1 is complemented ) by Def25;
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 &amp; b1 is transitive &amp; b1 is antisymmetric &amp; b1 is with_infima &amp; b1 is with_suprema &amp; b1 is bounded &amp; b1 is distributive &amp; b1 is complemented holds
b1 is Boolean by Def25;
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 &amp; b1 is Boolean &amp; not b1 is empty )
proofend;
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 &amp; b1 is Heyting &amp; not b1 is empty )
proofend;
end;