:: WAYBEL_1 semantic presentation

definition

let c₁, c₂ be non empty 1-sorted ;
let c₃ be Function of c₁,c₂;
redefine attr one-to-one as a₃ is one-to-one means :: WAYBEL_1:def 1
for b₁, b₂ being Element of a₁ st a₃ . b₁ = a₃ . b₂ holds
b₁ = b₂;
compatibility

proof end;

end;

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

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
redefine attr a₃ is monotone means :Def2: :: WAYBEL_1:def 2
for b₁, b₂ being Element of a₁ st b₁ <= b₂ holds
a₃ . b₁ <= a₃ . b₂;
compatibility

proof end;

end;

:: deftheorem Def2 defines monotone WAYBEL_1:def 2 :

theorem Th1: :: WAYBEL_1:1

canceled;

theorem Th2: :: WAYBEL_1:2

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ holds
b₂ "/\" b₄ <= b₃ "/\" b₄

proof end;

theorem Th3: :: WAYBEL_1:3

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ holds
b₂ "\/" b₄ <= b₃ "\/" b₄

proof end;

theorem Th4: :: WAYBEL_1:4

for b₁ being non empty antisymmetric lower-bounded RelStr
for b₂ being Element of b₁ holds
( ( b₁ is with_infima implies (Bottom b₁) "/\" b₂ = Bottom b₁ ) & ( b₁ is with_suprema & b₁ is reflexive & b₁ is transitive implies (Bottom b₁) "\/" b₂ = b₂ ) )

proof end;

theorem Th5: :: WAYBEL_1:5

for b₁ being non empty antisymmetric upper-bounded RelStr
for b₂ being Element of b₁ holds
( ( b₁ is with_infima & b₁ is transitive & b₁ is reflexive implies (Top b₁) "/\" b₂ = b₂ ) & ( b₁ is with_suprema implies (Top b₁) "\/" b₂ = Top b₁ ) )

proof end;

definition

let c₁ be non empty RelStr ;
attr a₁ is distributive means :Def3: :: WAYBEL_1:def 3
for b₁, b₂, b₃ being Element of a₁ holds b₁ "/\" (b₂ "\/" b₃) = (b₁ "/\" b₂) "\/" (b₁ "/\" b₃);

end;

:: deftheorem Def3 defines distributive WAYBEL_1:def 3 :

theorem Th6: :: WAYBEL_1:6

for b₁ being LATTICE holds
( b₁ is distributive iff for b₂, b₃, b₄ being Element of b₁ holds b₂ "\/" (b₃ "/\" b₄) = (b₂ "\/" b₃) "/\" (b₂ "\/" b₄) )

proof end;

registration

let c₁ be set ;
cluster BoolePoset a₁ -> distributive ;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be set ;
pred ex_min_of c₂,c₁ means :: WAYBEL_1:def 4
( ex_inf_of a₂,a₁ & "/\" a₂,a₁ in a₂ );
pred ex_max_of c₂,c₁ means :Def5: :: WAYBEL_1:def 5
( ex_sup_of a₂,a₁ & "\/" a₂,a₁ in a₂ );

end;

:: deftheorem Def4 defines ex_min_of WAYBEL_1:def 4 :

:: deftheorem Def5 defines ex_max_of WAYBEL_1:def 5 :

notation

let c₁ be non empty RelStr ;
let c₂ be set ;
synonym c₂ has_the_min_in c₁ for ex_min_of c₂,c₁;
synonym c₂ has_the_max_in c₁ for ex_max_of c₂,c₁;

end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
let c₃ be set ;
pred c₂ is_minimum_of c₃ means :Def6: :: WAYBEL_1:def 6
( ex_inf_of a₃,a₁ & a₂ = "/\" a₃,a₁ & "/\" a₃,a₁ in a₃ );
pred c₂ is_maximum_of c₃ means :Def7: :: WAYBEL_1:def 7
( ex_sup_of a₃,a₁ & a₂ = "\/" a₃,a₁ & "\/" a₃,a₁ in a₃ );

end;

:: deftheorem Def6 defines is_minimum_of WAYBEL_1:def 6 :

:: deftheorem Def7 defines is_maximum_of WAYBEL_1:def 7 :

registration

let c₁ be RelStr ;
cluster id a₁ -> isomorphic ;
coherence

proof end;

end;

definition

let c₁, c₂ be RelStr ;
pred c₁,c₂ are_isomorphic means :Def8: :: WAYBEL_1:def 8
ex b₁ being Function of a₁,a₂ st b₁ is isomorphic;
reflexivity

proof end;

end;

:: deftheorem Def8 defines are_isomorphic WAYBEL_1:def 8 :

theorem Th7: :: WAYBEL_1:7

for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic holds
b₂,b₁ are_isomorphic

proof end;

theorem Th8: :: WAYBEL_1:8

for b₁, b₂, b₃ being RelStr st b₁,b₂ are_isomorphic & b₂,b₃ are_isomorphic holds
b₁,b₃ are_isomorphic

proof end;

definition

let c₁, c₂ be RelStr ;
mode Connection of c₁,c₂ -> set means :Def9: :: WAYBEL_1:def 9
ex b₁ being Function of a₁,a₂ex b₂ being Function of a₂,a₁ st a₃ = [b₁,b₂];
existence

proof end;

end;

:: deftheorem Def9 defines Connection WAYBEL_1:def 9 :

definition

let c₁, c₂ be RelStr ;
let c₃ be Function of c₁,c₂;
let c₄ be Function of c₂,c₁;
redefine func [ as [c₃,c₄] -> Connection of a₁,a₂;
coherence by Def9;

end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Connection of c₁,c₂;
attr a₃ is Galois means :Def10: :: WAYBEL_1:def 10
ex b₁ being Function of a₁,a₂ex b₂ being Function of a₂,a₁ st
( a₃ = [b₁,b₂] & b₁ is monotone & b₂ is monotone & ( for b₃ being Element of a₂
for b₄ being Element of a₁ holds
( b₃ <= b₁ . b₄ iff b₂ . b₃ <= b₄ ) ) );

end;

:: deftheorem Def10 defines Galois WAYBEL_1:def 10 :

theorem Th9: :: WAYBEL_1:9

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ holds
( [b₃,b₄] is Galois iff ( b₃ is monotone & b₄ is monotone & ( for b₅ being Element of b₂
for b₆ being Element of b₁ holds
( b₅ <= b₃ . b₆ iff b₄ . b₅ <= b₆ ) ) ) )

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is upper_adjoint means :Def11: :: WAYBEL_1:def 11
ex b₁ being Function of a₂,a₁ st [a₃,b₁] is Galois;

end;

:: deftheorem Def11 defines upper_adjoint WAYBEL_1:def 11 :

notation

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
synonym c₃ has_a_lower_adjoint for upper_adjoint c₃;

end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₂,c₁;
attr a₃ is lower_adjoint means :Def12: :: WAYBEL_1:def 12
ex b₁ being Function of a₁,a₂ st [b₁,a₃] is Galois;

end;

:: deftheorem Def12 defines lower_adjoint WAYBEL_1:def 12 :

notation

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₂,c₁;
synonym c₃ has_an_upper_adjoint for lower_adjoint c₃;

end;

theorem Th10: :: WAYBEL_1:10

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st [b₃,b₄] is Galois holds
( b₃ is upper_adjoint & b₄ is lower_adjoint )

proof end;

theorem Th11: :: WAYBEL_1:11

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ holds
( [b₃,b₄] is Galois iff ( b₃ is monotone & ( for b₅ being Element of b₂ holds b₄ . b₅ is_minimum_of b₃ " (uparrow b₅) ) ) )

proof end;

theorem Th12: :: WAYBEL_1:12

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ holds
( [b₃,b₄] is Galois iff ( b₄ is monotone & ( for b₅ being Element of b₁ holds b₃ . b₅ is_maximum_of b₄ " (downarrow b₅) ) ) )

proof end;

theorem Th13: :: WAYBEL_1:13

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st b₃ is upper_adjoint holds
b₃ is infs-preserving

proof end;

registration

let c₁, c₂ be non empty Poset;
cluster upper_adjoint -> infs-preserving M4(the carrier of a₁,the carrier of a₂);
coherence by Th13;

end;

theorem Th14: :: WAYBEL_1:14

for b₁, b₂ being non empty Poset
for b₃ being Function of b₂,b₁ st b₃ is lower_adjoint holds
b₃ is sups-preserving

proof end;

registration

let c₁, c₂ be non empty Poset;
cluster lower_adjoint -> sups-preserving M4(the carrier of a₁,the carrier of a₂);
coherence by Th14;

end;

theorem Th15: :: WAYBEL_1:15

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st b₁ is complete & b₃ is infs-preserving holds
ex b₄ being Function of b₂,b₁ st
( [b₃,b₄] is Galois & ( for b₅ being Element of b₂ holds b₄ . b₅ is_minimum_of b₃ " (uparrow b₅) ) )

proof end;

theorem Th16: :: WAYBEL_1:16

for b₁, b₂ being non empty Poset
for b₃ being Function of b₂,b₁ st b₂ is complete & b₃ is sups-preserving holds
ex b₄ being Function of b₁,b₂ st
( [b₄,b₃] is Galois & ( for b₅ being Element of b₁ holds b₄ . b₅ is_maximum_of b₃ " (downarrow b₅) ) )

proof end;

theorem Th17: :: WAYBEL_1:17

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂ st b₁ is complete holds
( b₃ is infs-preserving iff ( b₃ is monotone & b₃ has_a_lower_adjoint ) )

proof end;

theorem Th18: :: WAYBEL_1:18

for b₁, b₂ being non empty Poset
for b₃ being Function of b₂,b₁ st b₂ is complete holds
( b₃ is sups-preserving iff ( b₃ is monotone & b₃ has_an_upper_adjoint ) )

proof end;

theorem Th19: :: WAYBEL_1:19

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st [b₃,b₄] is Galois holds
( b₄ * b₃ <= id b₁ & id b₂ <= b₃ * b₄ )

proof end;

theorem Th20: :: WAYBEL_1:20

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ is monotone & b₄ is monotone & b₄ * b₃ <= id b₁ & id b₂ <= b₃ * b₄ holds
[b₃,b₄] is Galois

proof end;

theorem Th21: :: WAYBEL_1:21

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ is monotone & b₄ is monotone & b₄ * b₃ <= id b₁ & id b₂ <= b₃ * b₄ holds
( b₄ = (b₄ * b₃) * b₄ & b₃ = (b₃ * b₄) * b₃ )

proof end;

theorem Th22: :: WAYBEL_1:22

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₄ = (b₄ * b₃) * b₄ & b₃ = (b₃ * b₄) * b₃ holds
( b₃ * b₄ is idempotent & b₄ * b₃ is idempotent )

proof end;

theorem Th23: :: WAYBEL_1:23

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st [b₃,b₄] is Galois & b₃ is onto holds
for b₅ being Element of b₂ holds b₄ . b₅ is_minimum_of b₃ " {b₅}

proof end;

theorem Th24: :: WAYBEL_1:24

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st ( for b₅ being Element of b₂ holds b₄ . b₅ is_minimum_of b₃ " {b₅} ) holds
b₃ * b₄ = id b₂

proof end;

theorem Th25: :: WAYBEL_1:25

for b₁, b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₄ * b₃ = id b₁ holds
( b₃ is one-to-one & b₄ is onto )

proof end;

theorem Th26: :: WAYBEL_1:26

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st [b₃,b₄] is Galois holds
( b₃ is onto iff b₄ is one-to-one )

proof end;

theorem Th27: :: WAYBEL_1:27

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st [b₃,b₄] is Galois & b₄ is onto holds
for b₅ being Element of b₁ holds b₃ . b₅ is_maximum_of b₄ " {b₅}

proof end;

theorem Th28: :: WAYBEL_1:28

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st ( for b₅ being Element of b₁ holds b₃ . b₅ is_maximum_of b₄ " {b₅} ) holds
b₄ * b₃ = id b₁

proof end;

theorem Th29: :: WAYBEL_1:29

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st [b₃,b₄] is Galois holds
( b₃ is one-to-one iff b₄ is onto )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Function of c₁,c₁;
attr a₂ is projection means :Def13: :: WAYBEL_1:def 13
( a₂ is idempotent & a₂ is monotone );

end;

:: deftheorem Def13 defines projection WAYBEL_1:def 13 :

notation

let c₁ be non empty RelStr ;
let c₂ be Function of c₁,c₁;
synonym c₂ is_a_projection_operator for projection c₂;

end;

registration

let c₁ be non empty RelStr ;
cluster id a₁ -> isomorphic projection ;
coherence

proof end;

end;

registration

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

proof end;

end;

definition

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

end;

:: deftheorem Def14 defines closure WAYBEL_1:def 14 :

notation

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

end;

registration

let c₁ be non empty RelStr ;
cluster closure -> projection M4(the carrier of a₁,the carrier of a₁);
coherence by Def14;

end;

Lemma36: for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₂ is reflexive holds
b₃ <= b₃

proof end;

registration

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

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster id a₁ -> isomorphic projection closure ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def15 defines kernel WAYBEL_1:def 15 :

notation

let c₁ be non empty RelStr ;
let c₂ be Function of c₁,c₁;
synonym c₂ is_a_kernel_operator for kernel c₂;

end;

registration

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

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

Lemma38: for b₁ being non empty 1-sorted
for b₂ being Function of b₁,b₁ st b₂ is idempotent holds
for b₃ being set st b₃ in rng b₂ holds
b₂ . b₃ = b₃

proof end;

theorem Th30: :: WAYBEL_1:30

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁
for b₃ being Subset of b₁ st b₂ is_a_closure_operator & ex_inf_of b₃,b₁ & b₃ c= rng b₂ holds
inf b₃ = b₂ . (inf b₃)

proof end;

theorem Th31: :: WAYBEL_1:31

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁
for b₃ being Subset of b₁ st b₂ is_a_kernel_operator & ex_sup_of b₃,b₁ & b₃ c= rng b₂ holds
sup b₃ = b₂ . (sup b₃)

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
func corestr c₃ -> Function of a₁,(Image a₃) equals :: WAYBEL_1:def 16
the carrier of (Image a₃) | a₃;
coherence

proof end;

end;

:: deftheorem Def16 defines corestr WAYBEL_1:def 16 :

theorem Th32: :: WAYBEL_1:32

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ holds corestr b₃ = b₃

proof end;

Lemma42: for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ holds corestr b₃ is onto

proof end;

registration

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
cluster corestr a₃ -> onto ;
coherence by Lemma42;

end;

theorem Th33: :: WAYBEL_1:33

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is monotone holds
corestr b₃ is monotone

proof end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
func inclusion c₃ -> Function of (Image a₃),a₂ equals :: WAYBEL_1:def 17
id (Image a₃);
coherence

proof end;

end;

:: deftheorem Def17 defines inclusion WAYBEL_1:def 17 :

theorem Th34: :: WAYBEL_1:34

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being Element of (Image b₃) holds (inclusion b₃) . b₄ = b₄ by TMAP_1:91;

Lemma45: for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ holds inclusion b₃ is monotone

proof end;

registration

let c₁, c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
cluster inclusion a₃ -> V5 monotone ;
coherence by Lemma45;

end;

theorem Th35: :: WAYBEL_1:35

for b₁ being non empty RelStr
for b₂ being Function of b₁,b₁ holds (inclusion b₂) * (corestr b₂) = b₂

proof end;

theorem Th36: :: WAYBEL_1:36

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is idempotent holds
(corestr b₂) * (inclusion b₂) = id (Image b₂)

proof end;

theorem Th37: :: WAYBEL_1:37

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
ex b₃ being non empty Posetex b₄ being Function of b₁,b₃ex b₅ being Function of b₃,b₁ st
( b₄ is monotone & b₄ is onto & b₅ is monotone & b₅ is one-to-one & b₂ = b₅ * b₄ & id b₃ = b₄ * b₅ )

proof end;

theorem Th38: :: WAYBEL_1:38

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st ex b₃ being non empty Posetex b₄ being Function of b₁,b₃ex b₅ being Function of b₃,b₁ st
( b₄ is monotone & b₅ is monotone & b₂ = b₅ * b₄ & id b₃ = b₄ * b₅ ) holds
b₂ is_a_projection_operator

proof end;

theorem Th39: :: WAYBEL_1:39

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_closure_operator holds
[(inclusion b₂),(corestr b₂)] is Galois

proof end;

theorem Th40: :: WAYBEL_1:40

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_closure_operator holds
ex b₃ being non empty Posetex b₄ being Function of b₃,b₁ex b₅ being Function of b₁,b₃ st
( [b₄,b₅] is Galois & b₂ = b₄ * b₅ )

proof end;

theorem Th41: :: WAYBEL_1:41

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is monotone & ex b₃ being non empty Posetex b₄ being Function of b₃,b₁ex b₅ being Function of b₁,b₃ st
( [b₄,b₅] is Galois & b₂ = b₄ * b₅ ) holds
b₂ is_a_closure_operator

proof end;

theorem Th42: :: WAYBEL_1:42

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_kernel_operator holds
[(corestr b₂),(inclusion b₂)] is Galois

proof end;

theorem Th43: :: WAYBEL_1:43

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_kernel_operator holds
ex b₃ being non empty Posetex b₄ being Function of b₁,b₃ex b₅ being Function of b₃,b₁ st
( [b₄,b₅] is Galois & b₂ = b₅ * b₄ )

proof end;

theorem Th44: :: WAYBEL_1:44

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is monotone & ex b₃ being non empty Posetex b₄ being Function of b₁,b₃ex b₅ being Function of b₃,b₁ st
( [b₄,b₅] is Galois & b₂ = b₅ * b₄ ) holds
b₂ is_a_kernel_operator

proof end;

theorem Th45: :: WAYBEL_1:45

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
rng b₂ = { b₃ where B is Element of b₁ : b₃ <= b₂ . b₃ } /\ { b₃ where B is Element of b₁ : b₂ . b₃ <= b₃ }

proof end;

theorem Th46: :: WAYBEL_1:46

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
( { b₃ where B is Element of b₁ : b₃ <= b₂ . b₃ } is non empty Subset of b₁ & { b₃ where B is Element of b₁ : b₂ . b₃ <= b₃ } is non empty Subset of b₁ )

proof end;

theorem Th47: :: WAYBEL_1:47

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
( rng (b₂ | { b₃ where B is Element of b₁ : b₃ <= b₂ . b₃ } ) = rng b₂ & rng (b₂ | { b₃ where B is Element of b₁ : b₂ . b₃ <= b₃ } ) = rng b₂ )

proof end;

theorem Th48: :: WAYBEL_1:48

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
for b₃, b₄ being non empty Subset of b₁ st b₃ = { b₅ where B is Element of b₁ : b₅ <= b₂ . b₅ } holds
b₂ | b₃ is Function of (subrelstr b₃),(subrelstr b₃)

proof end;

theorem Th49: :: WAYBEL_1:49

proof end;

theorem Th50: :: WAYBEL_1:50

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
for b₃ being non empty Subset of b₁ st b₃ = { b₄ where B is Element of b₁ : b₄ <= b₂ . b₄ } holds
for b₄ being Function of (subrelstr b₃),(subrelstr b₃) st b₄ = b₂ | b₃ holds
b₄ is_a_closure_operator

proof end;

theorem Th51: :: WAYBEL_1:51

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
for b₃ being non empty Subset of b₁ st b₃ = { b₄ where B is Element of b₁ : b₂ . b₄ <= b₄ } holds
for b₄ being Function of (subrelstr b₃),(subrelstr b₃) st b₄ = b₂ | b₃ holds
b₄ is_a_kernel_operator

proof end;

theorem Th52: :: WAYBEL_1:52

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is monotone holds
for b₃ being Subset of b₁ st b₃ = { b₄ where B is Element of b₁ : b₄ <= b₂ . b₄ } holds
subrelstr b₃ is sups-inheriting

proof end;

theorem Th53: :: WAYBEL_1:53

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is monotone holds
for b₃ being Subset of b₁ st b₃ = { b₄ where B is Element of b₁ : b₂ . b₄ <= b₄ } holds
subrelstr b₃ is infs-inheriting

proof end;

theorem Th54: :: WAYBEL_1:54

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
for b₃ being non empty Subset of b₁ st b₃ = { b₄ where B is Element of b₁ : b₄ <= b₂ . b₄ } holds
( ( b₂ is infs-preserving implies ( subrelstr b₃ is infs-inheriting & Image b₂ is infs-inheriting ) ) & ( b₂ is filtered-infs-preserving implies ( subrelstr b₃ is filtered-infs-inheriting & Image b₂ is filtered-infs-inheriting ) ) )

proof end;

theorem Th55: :: WAYBEL_1:55

for b₁ being non empty Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
for b₃ being non empty Subset of b₁ st b₃ = { b₄ where B is Element of b₁ : b₂ . b₄ <= b₄ } holds
( ( b₂ is sups-preserving implies ( subrelstr b₃ is sups-inheriting & Image b₂ is sups-inheriting ) ) & ( b₂ is directed-sups-preserving implies ( subrelstr b₃ is directed-sups-inheriting & Image b₂ is directed-sups-inheriting ) ) )

proof end;

theorem Th56: :: WAYBEL_1:56

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

proof end;

theorem Th57: :: WAYBEL_1:57

for b₁ being non empty complete Poset
for b₂ being Function of b₁,b₁ st b₂ is_a_projection_operator holds
Image b₂ is complete

proof end;

theorem Th58: :: WAYBEL_1:58

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

proof end;

theorem Th59: :: WAYBEL_1:59

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

proof end;

theorem Th60: :: WAYBEL_1:60

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

proof end;

theorem Th61: :: WAYBEL_1:61

for b₁ being non empty complete Poset holds
( (IdsMap b₁) * (SupMap b₁) is_a_closure_operator & Image ((IdsMap b₁) * (SupMap b₁)),b₁ are_isomorphic )

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
func c₂ "/\" -> Function of a₁,a₁ means :Def18: :: WAYBEL_1:def 18
for b₁ being Element of a₁ holds a₃ . b₁ = a₂ "/\" b₁;
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th62: :: WAYBEL_1:62

for b₁ being non empty RelStr
for b₂, b₃ being Element of b₁ holds { b₄ where B is Element of b₁ : b₂ "/\" b₄ <= b₃ } = (b₂ "/\" ) " (downarrow b₃)

proof end;

theorem Th63: :: WAYBEL_1:63

for b₁ being Semilattice
for b₂ being Element of b₁ holds b₂ "/\" is monotone

proof end;

registration

let c₁ be Semilattice;
let c₂ be Element of c₁;
cluster a₂ "/\" -> monotone ;
coherence by Th63;

end;

theorem Th64: :: WAYBEL_1:64

for b₁ being non empty RelStr
for b₂ being Element of b₁
for b₃ being Subset of b₁ holds (b₂ "/\" ) .: b₃ = { (b₂ "/\" b₄) where B is Element of b₁ : b₄ in b₃ }

proof end;

theorem Th65: :: WAYBEL_1:65

for b₁ being Semilattice holds
( ( for b₂ being Element of b₁ holds b₂ "/\" has_an_upper_adjoint ) iff for b₂, b₃ being Element of b₁ holds ex_max_of { b₄ where B is Element of b₁ : b₂ "/\" b₄ <= b₃ } ,b₁ )

proof end;

theorem Th66: :: WAYBEL_1:66

for b₁ being Semilattice st ( for b₂ being Element of b₁ holds b₂ "/\" has_an_upper_adjoint ) holds
for b₂ being Subset of b₁ st ex_sup_of b₂,b₁ holds
for b₃ being Element of b₁ holds b₃ "/\" ("\/" b₂,b₁) = "\/" { (b₃ "/\" b₄) where B is Element of b₁ : b₄ in b₂ } ,b₁

proof end;

theorem Th67: :: WAYBEL_1:67

for b₁ being non empty complete Poset holds
( ( for b₂ being Element of b₁ holds b₂ "/\" has_an_upper_adjoint ) iff for b₂ being Subset of b₁
for b₃ being Element of b₁ holds b₃ "/\" ("\/" b₂,b₁) = "\/" { (b₃ "/\" b₄) where B is Element of b₁ : b₄ in b₂ } ,b₁ )

proof end;

theorem Th68: :: WAYBEL_1:68

for b₁ being LATTICE st ( for b₂ being Subset of b₁ st ex_sup_of b₂,b₁ holds
for b₃ being Element of b₁ holds b₃ "/\" ("\/" b₂,b₁) = "\/" { (b₃ "/\" b₄) where B is Element of b₁ : b₄ in b₂ } ,b₁ ) holds
b₁ is distributive

proof end;

definition

let c₁ be non empty RelStr ;
attr a₁ is Heyting means :Def19: :: WAYBEL_1:def 19
( a₁ is LATTICE & ( for b₁ being Element of a₁ holds b₁ "/\" has_an_upper_adjoint ) );

end;

:: deftheorem Def19 defines Heyting WAYBEL_1:def 19 :

notation

let c₁ be non empty RelStr ;
synonym c₁ is_a_Heyting_algebra for Heyting c₁;

end;

registration

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

end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
assume E68: c₁ is Heyting ;
func c₂ => -> Function of a₁,a₁ means :Def20: :: WAYBEL_1:def 20
[a₃,(a₂ "/\" )] is Galois;
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th69: :: WAYBEL_1:69

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
b₁ is distributive

proof end;

registration

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

end;

definition

let c₁ be non empty RelStr ;
let c₂, c₃ be Element of c₁;
func c₂ => c₃ -> Element of a₁ equals :: WAYBEL_1:def 21
(a₂ => ) . a₃;
correctness ;

end;

:: deftheorem Def21 defines => WAYBEL_1:def 21 :

theorem Th70: :: WAYBEL_1:70

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ >= b₃ "/\" b₄ iff b₃ => b₂ >= b₄ )

proof end;

theorem Th71: :: WAYBEL_1:71

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
b₁ 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 b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃ being Element of b₁ holds
( Top b₁ = b₂ => b₃ iff b₂ <= b₃ )

proof end;

theorem Th73: :: WAYBEL_1:73

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂ being Element of b₁ holds Top b₁ = b₂ => b₂

proof end;

theorem Th74: :: WAYBEL_1:74

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃ being Element of b₁ st Top b₁ = b₂ => b₃ & Top b₁ = b₃ => b₂ holds
b₂ = b₃

proof end;

theorem Th75: :: WAYBEL_1:75

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃ being Element of b₁ holds b₃ <= b₂ => b₃

proof end;

theorem Th76: :: WAYBEL_1:76

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

proof end;

theorem Th77: :: WAYBEL_1:77

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

proof end;

Lemma74: for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃ being Element of b₁ holds b₂ "/\" (b₂ => b₃) <= b₃

proof end;

theorem Th78: :: WAYBEL_1:78

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃, b₄ being Element of b₁ st b₂ <= b₃ holds
b₃ => b₄ <= b₂ => b₄

proof end;

theorem Th79: :: WAYBEL_1:79

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃, b₄ being Element of b₁ st b₃ <= b₄ holds
b₂ => b₃ <= b₂ => b₄

proof end;

theorem Th80: :: WAYBEL_1:80

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃ being Element of b₁ holds b₂ "/\" (b₂ => b₃) = b₂ "/\" b₃

proof end;

theorem Th81: :: WAYBEL_1:81

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃, b₄ being Element of b₁ holds (b₂ "\/" b₃) => b₄ = (b₂ => b₄) "/\" (b₃ => b₄)

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be Element of c₁;
func 'not' c₂ -> Element of a₁ equals :: WAYBEL_1:def 22
a₂ => (Bottom a₁);
correctness ;

end;

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

theorem Th82: :: WAYBEL_1:82

for b₁ being non empty RelStr st b₁ is_a_Heyting_algebra & b₁ is lower-bounded holds
for b₂ being Element of b₁ holds 'not' b₂ is_maximum_of { b₃ where B is Element of b₁ : b₂ "/\" b₃ = Bottom b₁ }

proof end;

theorem Th83: :: WAYBEL_1:83

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

proof end;

theorem Th84: :: WAYBEL_1:84

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

proof end;

theorem Th85: :: WAYBEL_1:85

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

proof end;

theorem Th86: :: WAYBEL_1:86

for b₁ being non empty lower-bounded RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃ being Element of b₁ st b₂ <= b₃ holds
'not' b₃ <= 'not' b₂

proof end;

theorem Th87: :: WAYBEL_1:87

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

theorem Th88: :: WAYBEL_1:88

for b₁ being non empty lower-bounded RelStr st b₁ is_a_Heyting_algebra holds
for b₂, b₃ being Element of b₁ holds 'not' (b₂ "/\" b₃) >= ('not' b₂) "\/" ('not' b₃)

proof end;

definition

let c₁ be non empty RelStr ;
let c₂, c₃ be Element of c₁;
pred c₃ is_a_complement_of c₂ means :Def23: :: WAYBEL_1:def 23
( a₂ "\/" a₃ = Top a₁ & a₂ "/\" a₃ = Bottom a₁ );

end;

:: deftheorem Def23 defines is_a_complement_of WAYBEL_1:def 23 :

definition

let c₁ be non empty RelStr ;
attr a₁ is complemented means :Def24: :: WAYBEL_1:def 24
for b₁ being Element of a₁ ex b₂ being Element of a₁ st b₂ is_a_complement_of b₁;

end;

:: deftheorem Def24 defines complemented WAYBEL_1:def 24 :

registration

let c₁ be set ;
cluster BoolePoset a₁ -> distributive complemented ;
coherence

proof end;

end;

Lemma83: for b₁ being bounded LATTICE st b₁ is distributive & b₁ is complemented holds
for b₂ being Element of b₁ ex b₃ being Element of b₁ st
for b₄ being Element of b₁ holds
( (b₄ "\/" b₃) "/\" b₂ <= b₄ & b₄ <= (b₄ "/\" b₂) "\/" b₃ )

proof end;

Lemma84: for b₁ being bounded LATTICE st ( for b₂ being Element of b₁ ex b₃ being Element of b₁ st
for b₄ being Element of b₁ holds
( (b₄ "\/" b₃) "/\" b₂ <= b₄ & b₄ <= (b₄ "/\" b₂) "\/" b₃ ) ) holds
( b₁ is_a_Heyting_algebra & ( for b₂ being Element of b₁ holds 'not' ('not' b₂) = b₂ ) )

proof end;

theorem Th89: :: WAYBEL_1:89

for b₁ being bounded LATTICE st b₁ is_a_Heyting_algebra & ( for b₂ being Element of b₁ holds 'not' ('not' b₂) = b₂ ) holds
for b₂ being Element of b₁ holds 'not' b₂ is_a_complement_of b₂

proof end;

theorem Th90: :: WAYBEL_1:90

for b₁ being bounded LATTICE holds
( b₁ is distributive & b₁ is complemented iff ( b₁ is_a_Heyting_algebra & ( for b₂ being Element of b₁ holds 'not' ('not' b₂) = b₂ ) ) )

proof end;

definition