:: WAYBEL_1 semantic presentation

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

proof end;

end;

:: deftheorem defines one-to-one WAYBEL_1:def 1 :

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

proof end;

end;

:: deftheorem Def2 defines monotone WAYBEL_1:def 2 :

theorem :: WAYBEL_1:1

canceled;

theorem Th2: :: WAYBEL_1:2

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 Th3: :: WAYBEL_1:3

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 Th4: :: WAYBEL_1:4

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 Th5: :: WAYBEL_1:5

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 :

theorem Th6: :: WAYBEL_1:6

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

proof end;

registration

let X be set ;
cluster BoolePoset X -> distributive ;
coherence

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 :Def5: :: WAYBEL_1:def 5
( ex_sup_of X,S & "\/" X,S in X );

end;

:: deftheorem defines ex_min_of WAYBEL_1:def 4 :

:: deftheorem Def5 defines ex_max_of WAYBEL_1:def 5 :

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 :Def6: :: WAYBEL_1:def 6
( 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 );

end;

:: deftheorem Def6 defines is_minimum_of WAYBEL_1:def 6 :

:: deftheorem Def7 defines is_maximum_of WAYBEL_1:def 7 :

registration

let L be RelStr ;
cluster id L -> isomorphic ;
coherence

proof end;

end;

definition

let L1, L2 be RelStr ;
pred L1,L2 are_isomorphic means :Def8: :: WAYBEL_1:def 8
ex f being Function of L1,L2 st f is isomorphic;
reflexivity

proof end;

end;

:: deftheorem Def8 defines are_isomorphic WAYBEL_1:def 8 :

theorem :: WAYBEL_1:7

for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds
L2,L1 are_isomorphic

proof end;

theorem :: WAYBEL_1:8

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

proof end;

end;

:: deftheorem Def9 defines Connection WAYBEL_1:def 9 :

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

end;

definition

let S, T be non empty RelStr ;
let gc be Connection of S,T;
attr gc 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] & 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 Def10 defines Galois WAYBEL_1:def 10 :

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

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

end;

:: deftheorem Def11 defines upper_adjoint WAYBEL_1:def 11 :

notation

let S, T be non empty RelStr ;
let g be Function of S,T;
synonym g has_a_lower_adjoint for upper_adjoint g;

end;

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 :

notation

let S, T be non empty RelStr ;
let d be Function of T,S;
synonym d has_an_upper_adjoint for lower_adjoint d;

end;

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 st [g,d] is Galois holds
( g is upper_adjoint & d is lower_adjoint )

proof end;

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

proof end;

theorem Th12: :: WAYBEL_1:12

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 Th13: :: WAYBEL_1:13

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 upper_adjoint -> infs-preserving M4(the carrier of S,the carrier of T);
coherence by Th13;

end;

theorem Th14: :: WAYBEL_1:14

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 lower_adjoint -> sups-preserving M4(the carrier of S,the carrier of T);
coherence by Th14;

end;

theorem Th15: :: WAYBEL_1:15

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 Th16: :: WAYBEL_1:16

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;

theorem :: WAYBEL_1:17

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

proof end;

theorem Th18: :: WAYBEL_1:18

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

proof end;

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,d] is Galois holds
( d * g <= id S & id T <= g * d )

proof end;

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
[g,d] is Galois

proof end;

theorem Th21: :: WAYBEL_1:21

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 Th22: :: WAYBEL_1:22

for S, T being non empty RelStr
for g being Function of S,T
for d being Function of T,S st d = (d * g) * d & g = (g * d) * g holds
( g * d is idempotent & d * g is idempotent )

proof end;

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 [g,d] is Galois & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}

proof end;

theorem Th24: :: 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 ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds
g * d = id T

proof end;

theorem Th25: :: WAYBEL_1:25

for L1, L2 being non empty 1-sorted
for g1 being Function of L1,L2
for g2 being Function of L2,L1 st g2 * g1 = id L1 holds
( g1 is one-to-one & g2 is onto )

proof end;

theorem :: 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 [g,d] is Galois holds
( g is onto iff d is one-to-one )

proof end;

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

proof end;

theorem Th28: :: WAYBEL_1:28

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;

theorem :: WAYBEL_1:29

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 one-to-one iff d is onto )

proof end;

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 :

notation

let L be non empty RelStr ;
let p be Function of L,L;
synonym p is_a_projection_operator for projection p;

end;

registration

let L be non empty RelStr ;
cluster id L -> isomorphic projection ;
coherence

proof end;

end;

registration

let L be non empty RelStr ;
cluster projection M4(the carrier of L,the carrier of L);
existence

proof end;

end;

definition

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

end;

:: deftheorem Def14 defines closure WAYBEL_1:def 14 :

notation

let L be non empty RelStr ;
let c be Function of L,L;
synonym c is_a_closure_operator for closure c;

end;

registration

let L be non empty RelStr ;
cluster closure -> projection M4(the carrier of L,the carrier of L);
coherence 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

proof end;

registration

let L be non empty reflexive RelStr ;
cluster projection closure M4(the carrier of L,the carrier of L);
existence

proof end;

end;

registration

let L be non empty reflexive RelStr ;
cluster id L -> isomorphic projection closure ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def15 defines kernel WAYBEL_1:def 15 :

notation

let L be non empty RelStr ;
let k be Function of L,L;
synonym k is_a_kernel_operator for kernel k;

end;

registration

let L be non empty RelStr ;
cluster kernel -> projection M4(the carrier of L,the carrier of L);
coherence by Def15;

end;

registration

let L be non empty reflexive RelStr ;
cluster projection kernel M4(the carrier of L,the carrier of L);
existence

proof end;

end;

registration

let L be non empty reflexive RelStr ;
cluster id L -> isomorphic projection closure kernel ;
coherence

proof end;

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 Th30: :: WAYBEL_1:30

for L being non empty Poset
for c being Function of L,L
for X being Subset of L st c is_a_closure_operator & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)

proof end;

theorem Th31: :: WAYBEL_1:31

for L being non empty Poset
for k being Function of L,L
for X being Subset of L st k is_a_kernel_operator & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)

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

proof end;

end;

:: deftheorem defines corestr WAYBEL_1:def 16 :

theorem Th32: :: WAYBEL_1:32

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

end;

theorem Th33: :: WAYBEL_1:33

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

proof end;

end;

:: deftheorem defines inclusion WAYBEL_1:def 17 :

theorem Th34: :: WAYBEL_1:34

for L1, L2 being non empty RelStr
for g being Function of L1,L2
for s being Element of (Image g) holds (inclusion g) . s = s by TMAP_1:91;

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;
cluster inclusion g -> V5 monotone ;
coherence by Lm4;

end;

theorem Th35: :: WAYBEL_1:35

for L being non empty RelStr
for f being Function of L,L holds (inclusion f) * (corestr f) = f

proof end;

theorem Th36: :: WAYBEL_1:36

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

for L being non empty Poset
for f being Function of L,L st f is_a_projection_operator 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 one-to-one & f = i * q & id T = q * i )

proof end;

theorem :: WAYBEL_1:38

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_a_projection_operator

proof end;

theorem Th39: :: WAYBEL_1:39

for L being non empty Poset
for f being Function of L,L st f is_a_closure_operator holds
[(inclusion f),(corestr f)] is Galois

proof end;

theorem :: WAYBEL_1:40

for L being non empty Poset
for f being Function of L,L st f is_a_closure_operator 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 Th41: :: WAYBEL_1:41

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_a_closure_operator

proof end;

theorem Th42: :: WAYBEL_1:42

for L being non empty Poset
for f being Function of L,L st f is_a_kernel_operator holds
[(corestr f),(inclusion f)] is Galois

proof end;

theorem :: WAYBEL_1:43

for L being non empty Poset
for f being Function of L,L st f is_a_kernel_operator 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 :: WAYBEL_1:44

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_a_kernel_operator

proof end;

theorem Th45: :: WAYBEL_1:45

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator holds
rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }

proof end;

theorem Th46: :: WAYBEL_1:46

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator holds
( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L )

proof end;

theorem Th47: :: WAYBEL_1:47

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator holds
( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p )

proof end;

theorem Th48: :: WAYBEL_1:48

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator 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:49

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator 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;

theorem Th50: :: WAYBEL_1:50

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator 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_a_closure_operator

proof end;

theorem :: WAYBEL_1:51

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator 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_a_kernel_operator

proof end;

theorem Th52: :: WAYBEL_1:52

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;

theorem Th53: :: WAYBEL_1:53

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;

theorem :: WAYBEL_1:54

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator 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;

theorem :: WAYBEL_1:55

for L being non empty Poset
for p being Function of L,L st p is_a_projection_operator 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;

theorem Th56: :: WAYBEL_1:56

for L being non empty Poset
for p being Function of L,L holds
( ( p is_a_closure_operator implies Image p is infs-inheriting ) & ( p is_a_kernel_operator implies Image p is sups-inheriting ) )

proof end;

theorem :: WAYBEL_1:57

for L being non empty complete Poset
for p being Function of L,L st p is_a_projection_operator holds
Image p is complete

proof end;

theorem :: WAYBEL_1:58

for L being non empty Poset
for c being Function of L,L st c is_a_closure_operator holds
( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" X,(Image c) = c . ("\/" X,L) ) ) )

proof end;

theorem :: WAYBEL_1:59

for L being non empty Poset
for k being Function of L,L st k is_a_kernel_operator holds
( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" X,(Image k) = k . ("/\" X,L) ) ) )

proof end;

theorem Th60: :: WAYBEL_1:60

for L being non empty complete Poset holds
( [(IdsMap L),(SupMap L)] is Galois & SupMap L is sups-preserving )

proof end;

theorem :: WAYBEL_1:61

for L being non empty complete Poset holds
( (IdsMap L) * (SupMap L) is_a_closure_operator & 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

proof end;

uniqueness

proof end;

end;

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

theorem Th62: :: WAYBEL_1:62

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 Th63: :: WAYBEL_1:63

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

end;

theorem Th64: :: WAYBEL_1:64

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;

theorem Th65: :: WAYBEL_1:65

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

proof end;

theorem Th66: :: WAYBEL_1:66

for S being Semilattice st ( for x being Element of S holds x "/\" has_an_upper_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;

theorem :: WAYBEL_1:67

for S being non empty complete Poset holds
( ( for x being Element of S holds x "/\" has_an_upper_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;

theorem Th68: :: WAYBEL_1:68

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 :Def19: :: WAYBEL_1:def 19
( H is LATTICE & ( for x being Element of H holds x "/\" has_an_upper_adjoint ) );

end;

:: deftheorem Def19 defines Heyting WAYBEL_1:def 19 :

notation

let H be non empty RelStr ;
synonym H is_a_Heyting_algebra for Heyting H;

end;

registration

cluster non empty Heyting -> non empty reflexive transitive antisymmetric with_suprema with_infima RelStr ;
coherence by Def19;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines => WAYBEL_1:def 20 :

theorem Th69: :: WAYBEL_1:69

for H being non empty RelStr st H is_a_Heyting_algebra holds
H is distributive

proof end;

registration

cluster non empty Heyting -> non empty distributive RelStr ;
coherence by Th69;

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 ;

end;

:: deftheorem defines => WAYBEL_1:def 21 :

theorem Th70: :: WAYBEL_1:70

for H being non empty RelStr st H is_a_Heyting_algebra holds
for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y )

proof end;

theorem Th71: :: WAYBEL_1:71

for H being non empty RelStr st H is_a_Heyting_algebra holds
H is upper-bounded

proof end;

registration

cluster non empty Heyting -> non empty upper-bounded RelStr ;
coherence by Th71;

end;

theorem Th72: :: WAYBEL_1:72

for H being non empty RelStr st H is_a_Heyting_algebra holds
for a, b being Element of H holds
( Top H = a => b iff a <= b )

proof end;

theorem :: WAYBEL_1:73

for H being non empty RelStr st H is_a_Heyting_algebra holds
for a being Element of H holds Top H = a => a

proof end;

theorem :: WAYBEL_1:74

for H being non empty RelStr st H is_a_Heyting_algebra holds
for a, b being Element of H st Top H = a => b & Top H = b => a holds
a = b

proof end;

theorem Th75: :: WAYBEL_1:75

for H being non empty RelStr st H is_a_Heyting_algebra holds
for a, b being Element of H holds b <= a => b

proof end;

theorem :: WAYBEL_1:76

for H being non empty RelStr st H is_a_Heyting_algebra holds
for a being Element of H holds Top H = a => (Top H)

proof end;

theorem :: WAYBEL_1:77

for H being non empty RelStr st H is_a_Heyting_algebra holds
for b being Element of H holds b = (Top H) => b

proof end;

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

proof end;

theorem Th78: :: WAYBEL_1:78

for H being non empty RelStr st H is_a_Heyting_algebra holds
for a, b, c being Element of H st a <= b holds
b => c <= a => c

proof end;

theorem :: WAYBEL_1:79

for H being non empty RelStr st H is_a_Heyting_algebra holds
for a, b, c being Element of H st b <= c holds
a => b <= a => c

proof end;

theorem Th80: :: WAYBEL_1:80

for H being non empty RelStr st H is_a_Heyting_algebra holds
for a, b being Element of H holds a "/\" (a => b) = a "/\" b

proof end;

theorem Th81: :: WAYBEL_1:81

for H being non empty RelStr st H is_a_Heyting_algebra 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 ;

end;

:: deftheorem defines 'not' WAYBEL_1:def 22 :

theorem :: WAYBEL_1:82

for H being non empty RelStr st H is_a_Heyting_algebra & 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 Th83: :: WAYBEL_1:83

for H being non empty RelStr st H is_a_Heyting_algebra & H is lower-bounded holds
( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H )

proof end;

theorem :: WAYBEL_1:84

for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra holds
for a, b being Element of H holds
( 'not' a >= b iff 'not' b >= a )

proof end;

theorem Th85: :: WAYBEL_1:85

for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra holds
for a, b being Element of H holds
( 'not' a >= b iff a "/\" b = Bottom H )

proof end;

theorem :: WAYBEL_1:86

for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra holds
for a, b being Element of H st a <= b holds
'not' b <= 'not' a

proof end;

theorem Th87: :: WAYBEL_1:87

for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra holds
for a, b being Element of H holds 'not' (a "\/" b) = ('not' a) "/\" ('not' b) by Th81;

theorem :: WAYBEL_1:88

for H being non empty lower-bounded RelStr st H is_a_Heyting_algebra 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 :Def23: :: WAYBEL_1:def 23
( x "\/" y = Top L & x "/\" y = Bottom L );

end;

:: deftheorem Def23 defines is_a_complement_of WAYBEL_1:def 23 :

definition

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

end;

:: deftheorem Def24 defines complemented WAYBEL_1:def 24 :

registration

let X be set ;
cluster BoolePoset X -> distributive complemented ;
coherence

proof end;

end;

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

proof end;

Lm7: for L being bounded LATTICE st ( for x being Element of L ex x' being Element of L st
for y being Element of L holds
( (y "\/" x') "/\" x <= y & y <= (y "/\" x) "\/" x' ) ) holds
( L is_a_Heyting_algebra & ( for x being Element of L holds 'not' ('not' x) = x ) )

proof end;

theorem Th89: :: WAYBEL_1:89