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

( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds

x = y )

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

( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds

x = y )

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

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;

( f is monotone iff for x, y being Element of L1 st x <= y holds

f . x <= f . y )

end;
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 for x, y being Element of L1 st x <= y holds

f . x <= f . y;

( f is monotone iff for x, y being Element of L1 st x <= y holds

f . x <= f . y )

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

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

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

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

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

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 ;

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

for x, y, z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z);

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

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

( L is distributive iff for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) )

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

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 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 & "\/" (X,S) in X ) );

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

definition

let S be non empty RelStr ;

let s be Element of S;

let X be set ;

end;
let s be Element of S;

let X be set ;

pred s is_minimum_of X means :Def6: :: WAYBEL_1:def 6

( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X );

( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X );

pred s is_maximum_of X means :Def7: :: WAYBEL_1:def 7

( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X );

( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X );

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

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

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

definition

let L1, L2 be RelStr ;

for L1 being RelStr ex f being Function of L1,L1 st f is isomorphic

end;
pred L1,L2 are_isomorphic means :Def8: :: WAYBEL_1:def 8

ex f being Function of L1,L2 st f is isomorphic ;

reflexivity ex f being Function of L1,L2 st f is isomorphic ;

for L1 being RelStr ex f being Function of L1,L1 st f is isomorphic

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

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

for L1, L2, L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds

L1,L3 are_isomorphic

L1,L3 are_isomorphic

proof end;

begin

definition

let S, T be RelStr ;

ex b_{1} being set ex g being Function of S,T ex d being Function of T,S st b_{1} = [g,d]

end;
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 g being Function of S,T ex d being Function of T,S st it = [g,d];

ex b

proof end;

:: deftheorem Def9 defines Connection WAYBEL_1:def 9 :

for S, T being RelStr

for b_{3} being set holds

( b_{3} is Connection of S,T iff ex g being Function of S,T ex d being Function of T,S st b_{3} = [g,d] );

for S, T being RelStr

for b

( b

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

:: Definition 3.1

:: 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] & 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 ) ) ) );

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

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;

end;
let g be Function of S,T;

attr g is upper_adjoint means :Def11: :: WAYBEL_1:def 11

ex d being Function of T,S st [g,d] is Galois ;

ex d being Function of T,S st [g,d] is Galois ;

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

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;

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

ex g being Function of S,T st [g,d] is Galois ;

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

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 & d is lower_adjoint )

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 )

proof end;

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

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

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

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;

for b_{1} being Function of S,T st b_{1} is upper_adjoint holds

b_{1} is infs-preserving
by Th12;

end;
cluster Function-like quasi_total upper_adjoint -> infs-preserving for M2( bool [: the carrier of S, the carrier of T:]);

coherence for b

b

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

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;

for b_{1} being Function of S,T st b_{1} is lower_adjoint holds

b_{1} is sups-preserving
by Th13;

end;
cluster Function-like quasi_total lower_adjoint -> sups-preserving for M2( bool [: the carrier of S, the carrier of T:]);

coherence for b

b

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

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

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

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

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 )

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

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 )

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

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}

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

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() )

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}

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

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 )

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)

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

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

registration

let L be non empty RelStr ;

ex b_{1} being Function of L,L st b_{1} is projection

end;
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 b

proof end;

:: Definition 3.8 (ii)

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

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 ;

for b_{1} being Function of L,L st b_{1} is closure holds

b_{1} is projection
by Def14;

end;
cluster Function-like quasi_total closure -> projection for M2( bool [: the carrier of L, the carrier of L:]);

coherence for b

b

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 ;

ex b_{1} being Function of L,L st b_{1} is closure

end;
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 b

proof end;

:: Definition 3.8 (iii)

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

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 ;

for b_{1} being Function of L,L st b_{1} is kernel holds

b_{1} is projection
by Def15;

end;
cluster Function-like quasi_total kernel -> projection for M2( bool [: the carrier of L, the carrier of L:]);

coherence for b

b

registration

let L be non empty reflexive RelStr ;

ex b_{1} being Function of L,L st b_{1} is kernel

end;
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 b

proof end;

registration
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)

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)

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;

coherence

the carrier of (Image g) |` g is Function of L1,(Image g)

end;
let g be Function of L1,L2;

coherence

the carrier of (Image g) |` g is Function of L1,(Image g)

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

for L1, L2 being non empty RelStr

for g being Function of L1,L2 holds corestr g = the carrier of (Image g) |` g;

Lm3: for L1, L2 being non empty RelStr

for g being Function of L1,L2 holds corestr g is onto

proof end;

registration
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

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;

coherence

id (Image g) is Function of (Image g),L2

end;
let g be Function of L1,L2;

coherence

id (Image g) is Function of (Image g),L2

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

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

proof end;

registration

let L1, L2 be non empty RelStr ;

let g be Function of L1,L2;

coherence

( inclusion g is one-to-one & inclusion g is monotone ) by Lm4;

end;
let g be Function of L1,L2;

coherence

( inclusion g is one-to-one & inclusion g is monotone ) by Lm4;

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

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 )

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

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

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 )

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

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

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 )

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

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 }

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 )

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 )

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)

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)

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

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

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

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

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

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

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

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

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

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

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;

begin

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

( [(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 )

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

ex b_{1} being Function of S,S st

for s being Element of S holds b_{1} . s = x "/\" s

for b_{1}, b_{2} being Function of S,S st ( for s being Element of S holds b_{1} . s = x "/\" s ) & ( for s being Element of S holds b_{2} . s = x "/\" s ) holds

b_{1} = b_{2}

end;
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 for s being Element of S holds it . s = x "/\" s;

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def18 defines "/\" WAYBEL_1:def 18 :

for S being non empty RelStr

for x being Element of S

for b_{3} being Function of S,S holds

( b_{3} = x "/\" iff for s being Element of S holds b_{3} . s = x "/\" s );

for S being non empty RelStr

for x being Element of S

for b

( b

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)

for x, t being Element of S holds { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t)

proof 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 }

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 )

( ( 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)

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

( ( 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

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 ;

end;
attr H is Heyting means :Def19: :: WAYBEL_1:def 19

( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) );

( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) );

:: deftheorem Def19 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 ) ) );

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

for b_{1} being non empty RelStr st b_{1} is Heyting holds

( b_{1} is with_infima & b_{1} is with_suprema & b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric )
by Def19;

end;

cluster non empty Heyting -> non empty reflexive transitive antisymmetric with_suprema with_infima for RelStr ;

coherence for b

( b

definition

let H be non empty RelStr ;

let a be Element of H;

assume A1: H is Heyting ;

existence

ex b_{1} being Function of H,H st [b_{1},(a "/\")] is Galois

for b_{1}, b_{2} being Function of H,H st [b_{1},(a "/\")] is Galois & [b_{2},(a "/\")] is Galois holds

b_{1} = b_{2}

end;
let a be Element of H;

assume A1: H is Heyting ;

existence

ex b

proof end;

uniqueness for b

b

proof 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 b_{3} being Function of H,H holds

( b_{3} = a => iff [b_{3},(a "/\")] is Galois );

for H being non empty RelStr

for a being Element of H st H is Heyting holds

for b

( b

registration
end;

definition

let H be non empty RelStr ;

let a, y be Element of H;

correctness

coherence

(a =>) . y is Element of H;

;

end;
let a, y be Element of H;

correctness

coherence

(a =>) . y is Element of H;

;

:: deftheorem defines => WAYBEL_1:def 21 :

for H being non empty RelStr

for a, y being Element of H holds a => y = (a =>) . y;

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 )

for x, a, y being Element of H holds

( x >= a "/\" y iff a => x >= y )

proof end;

registration

coherence

for b_{1} being non empty RelStr st b_{1} is Heyting holds

b_{1} is upper-bounded
by Th68;

end;
for b

b

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 )

for a, b being Element of H holds

( Top H = a => b iff a <= b )

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

for a, b being Element of H st Top H = a => b & Top H = b => a holds

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)

for a being Element of H holds Top H = a => (Top H)

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

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

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

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)

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;

correctness

coherence

a => (Bottom H) is Element of H;

;

end;
let a be Element of H;

correctness

coherence

a => (Bottom H) is Element of H;

;

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

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 }

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 )

( '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 )

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 )

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

for a, b being Element of H st a <= b holds

'not' b <= 'not' a

proof end;

theorem :: WAYBEL_1:84

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)

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;

end;
let x, y be Element of L;

pred y is_a_complement_of x means :Def23: :: WAYBEL_1:def 23

( x "\/" y = Top L & x "/\" y = Bottom L );

( x "\/" y = Top L & x "/\" y = Bottom L );

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

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 ;

end;
attr L 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;

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

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

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

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

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

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

end;
attr B is Boolean means :Def25: :: WAYBEL_1:def 25

( B is LATTICE & B is bounded & B is distributive & B is complemented );

( B is LATTICE & B is bounded & B is distributive & B is complemented );

:: deftheorem Def25 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 ) );

for B being non empty RelStr holds

( B is Boolean iff ( B is LATTICE & B is bounded & B is distributive & B is complemented ) );

registration

for b_{1} being non empty RelStr st b_{1} is Boolean holds

( b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is with_infima & b_{1} is with_suprema & b_{1} is bounded & b_{1} is distributive & b_{1} is complemented )
by Def25;

end;

cluster non empty Boolean -> non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented for RelStr ;

coherence for b

( b

registration

for b_{1} being non empty RelStr st b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is with_infima & b_{1} is with_suprema & b_{1} is bounded & b_{1} is distributive & b_{1} is complemented holds

b_{1} is Boolean
by Def25;

end;

cluster non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented -> non empty Boolean for RelStr ;

coherence for b

b

registration
end;

registration

ex b_{1} being LATTICE st

( b_{1} is strict & b_{1} is Boolean & not b_{1} is empty )
end;

cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Boolean for RelStr ;

existence ex b

( b

proof end;

registration

ex b_{1} being LATTICE st

( b_{1} is strict & b_{1} is Heyting & not b_{1} is empty )
end;

cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Heyting for RelStr ;

existence ex b

( b

proof end;