:: WAYBEL10 semantic presentation

scheme :: WAYBEL10:sch 1
s1{ F₁() -> non empty RelStr , P₁[ set ], F₂() -> set } :

ex b₁ being non empty strict full SubRelStr of F₁() st
for b₂ being Element of F₁() holds
( b₂ is Element of b₁ iff P₁[b₂] )

provided

E1: P₁[F₂()] and
E2: F₂() in the carrier of F₁()

proof end;

scheme :: WAYBEL10:sch 2
s2{ F₁() -> non empty RelStr , F₂() -> non empty RelStr , P₁[ set ], P₂[ set , set ] } :

RelStr(# the carrier of F₁(),the InternalRel of F₁() #) = RelStr(# the carrier of F₂(),the InternalRel of F₂() #)

provided

E1: for b₁ being set holds
( b₁ is Element of F₁() iff P₁[b₁] ) and
E2: for b₁ being set holds
( b₁ is Element of F₂() iff P₁[b₁] ) and
E3: for b₁, b₂ being Element of F₁() holds
( b₁ <= b₂ iff P₂[b₁,b₂] ) and
E4: for b₁, b₂ being Element of F₂() holds
( b₁ <= b₂ iff P₂[b₁,b₂] )

proof end;

scheme :: WAYBEL10:sch 3
s3{ F₁() -> non empty RelStr , F₂() -> non empty full SubRelStr of F₁(), F₃() -> non empty full SubRelStr of F₁(), P₁[ set ] } :

RelStr(# the carrier of F₂(),the InternalRel of F₂() #) = RelStr(# the carrier of F₃(),the InternalRel of F₃() #)

provided

E1: for b₁ being set holds
( b₁ is Element of F₂() iff P₁[b₁] ) and
E2: for b₁ being set holds
( b₁ is Element of F₃() iff P₁[b₁] )

proof end;

scheme :: WAYBEL10:sch 4
s4{ F₁() -> non empty RelStr , F₂() -> non empty full SubRelStr of F₁(), F₃() -> non empty full SubRelStr of F₁(), P₁[ set ] } :

RelStr(# the carrier of F₂(),the InternalRel of F₂() #) = RelStr(# the carrier of F₃(),the InternalRel of F₃() #)

provided

E1: for b₁ being Element of F₁() holds
( b₁ is Element of F₂() iff P₁[b₁] ) and
E2: for b₁ being Element of F₁() holds
( b₁ is Element of F₃() iff P₁[b₁] )

proof end;

theorem Th1: :: WAYBEL10:1

for b₁, b₂ being Relation holds
( ( b₁ c= b₂ implies b₁ ~ c= b₂ ~ ) & ( b₁ ~ c= b₂ ~ implies b₁ c= b₂ ) & ( b₁ ~ c= b₂ implies b₁ c= b₂ ~ ) & ( b₁ c= b₂ ~ implies b₁ ~ c= b₂ ) )

proof end;

theorem Th2: :: WAYBEL10:2

canceled;

theorem Th3: :: WAYBEL10:3

for b₁, b₂ being RelStr holds
( ( b₂ is SubRelStr of b₁ implies b₂ opp is SubRelStr of b₁ opp ) & ( b₂ opp is SubRelStr of b₁ opp implies b₂ is SubRelStr of b₁ ) & ( b₂ opp is SubRelStr of b₁ implies b₂ is SubRelStr of b₁ opp ) & ( b₂ is SubRelStr of b₁ opp implies b₂ opp is SubRelStr of b₁ ) )

proof end;

theorem Th4: :: WAYBEL10:4

for b₁, b₂ being RelStr holds
( ( b₂ is full SubRelStr of b₁ implies b₂ opp is full SubRelStr of b₁ opp ) & ( b₂ opp is full SubRelStr of b₁ opp implies b₂ is full SubRelStr of b₁ ) & ( b₂ opp is full SubRelStr of b₁ implies b₂ is full SubRelStr of b₁ opp ) & ( b₂ is full SubRelStr of b₁ opp implies b₂ opp is full SubRelStr of b₁ ) )

proof end;

definition

let c₁ be RelStr ;
let c₂ be full SubRelStr of c₁;
redefine func ~ as c₂ opp -> strict full SubRelStr of a₁ opp ;
coherence by Th4;

end;

registration

let c₁ be set ;
let c₂ be non empty RelStr ;
cluster K104(a₁,a₂) -> non-Empty ;
coherence

proof end;

end;

registration

let c₁ be RelStr ;
let c₂ be non empty reflexive RelStr ;
cluster monotone Relation of the carrier of a₁,the carrier of a₂;
existence

proof end;

end;

registration

let c₁ be non empty RelStr ;
cluster projection -> idempotent monotone Relation of the carrier of a₁,the carrier of a₁;
coherence by WAYBEL_1:def 13;

end;

registration

let c₁, c₂ be non empty reflexive RelStr ;
let c₃ be monotone Function of c₁,c₂;
cluster corestr a₃ -> monotone ;
coherence

proof end;

end;

registration

let c₁ be 1-sorted ;
cluster id a₁ -> one-to-one ;
coherence

proof end;

end;

registration

let c₁ be non empty reflexive RelStr ;
cluster id a₁ -> idempotent infs-preserving sups-preserving ;
coherence

proof end;

end;

theorem Th5: :: WAYBEL10:5

for b₁ being RelStr
for b₂ being Subset of b₁ holds
( id b₂ is Function of (subrelstr b₂),b₁ & ( for b₃ being Function of (subrelstr b₂),b₁ st b₃ = id b₂ holds
b₃ is monotone ) )

proof end;

registration

let c₁ be non empty reflexive RelStr ;
cluster V5 idempotent monotone infs-preserving sups-preserving closure kernel Relation of the carrier of a₁,the carrier of a₁;
existence

proof end;

end;

theorem Th6: :: WAYBEL10:6

for b₁ being non empty reflexive RelStr
for b₂ being closure Function of b₁,b₁
for b₃ being Element of b₁ holds b₂ . b₃ >= b₃

proof end;

definition

let c₁, c₂ be 1-sorted ;
let c₃ be Function of the carrier of c₁,the carrier of c₂;
let c₄ be 1-sorted ;
assume E5: the carrier of c₄ c= the carrier of c₁ ;
func c₃ | c₄ -> Function of a₄,a₂ equals :Def1: :: WAYBEL10:def 1
a₃ | the carrier of a₄;
coherence

proof end;

correctness ;

end;

:: deftheorem Def1 defines | WAYBEL10:def 1 :

theorem Th7: :: WAYBEL10:7

for b₁, b₂ being RelStr
for b₃ being SubRelStr of b₁
for b₄ being Function of the carrier of b₁,the carrier of b₂ holds
( b₄ | b₃ = b₄ | the carrier of b₃ & ( for b₅ being set st b₅ in the carrier of b₃ holds
(b₄ | b₃) . b₅ = b₄ . b₅ ) )

proof end;

theorem Th8: :: WAYBEL10:8

for b₁, b₂ being RelStr
for b₃ being Function of b₁,b₂ st b₃ is one-to-one holds
for b₄ being SubRelStr of b₁ holds b₃ | b₄ is one-to-one

proof end;

registration

let c₁, c₂ be non empty reflexive RelStr ;
let c₃ be monotone Function of c₁,c₂;
let c₄ be SubRelStr of c₁;
cluster a₃ | a₄ -> monotone ;
coherence

proof end;

end;

theorem Th9: :: WAYBEL10:9

for b₁, b₂ being non empty RelStr
for b₃ being non empty SubRelStr of b₁
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₁ st b₄ is one-to-one & b₅ = b₄ " holds
( b₅ | (Image (b₄ | b₃)) is Function of (Image (b₄ | b₃)),b₃ & b₅ | (Image (b₄ | b₃)) = (b₄ | b₃) " )

proof end;

registration

let c₁ be RelStr ;
let c₂ be non empty reflexive RelStr ;
cluster MonMaps a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th10: :: WAYBEL10:10

for b₁ being RelStr
for b₂ being non empty reflexive RelStr
for b₃ being set holds
( b₃ is Element of (MonMaps b₁,b₂) iff b₃ is monotone Function of b₁,b₂ )

proof end;

definition

let c₁ be non empty reflexive RelStr ;
func ClOpers c₁ -> non empty strict full SubRelStr of MonMaps a₁,a₁ means :Def2: :: WAYBEL10:def 2
for b₁ being Function of a₁,a₁ holds
( b₁ is Element of a₂ iff b₁ is closure );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def2 defines ClOpers WAYBEL10:def 2 :

theorem Th11: :: WAYBEL10:11

for b₁ being non empty reflexive RelStr
for b₂ being set holds
( b₂ is Element of (ClOpers b₁) iff b₂ is closure Function of b₁,b₁ )

proof end;

theorem Th12: :: WAYBEL10:12

for b₁ being set
for b₂ being non empty RelStr
for b₃, b₄ being Function of b₁,the carrier of b₂
for b₅, b₆ being Element of (b₂ |^ b₁) st b₅ = b₃ & b₆ = b₄ holds
( b₅ <= b₆ iff b₃ <= b₄ )

proof end;

theorem Th13: :: WAYBEL10:13

for b₁ being complete LATTICE
for b₂, b₃ being Function of b₁,b₁
for b₄, b₅ being Element of (ClOpers b₁) st b₄ = b₂ & b₅ = b₃ holds
( b₄ <= b₅ iff b₂ <= b₃ )

proof end;

theorem Th14: :: WAYBEL10:14

for b₁ being reflexive RelStr
for b₂, b₃ being full SubRelStr of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is SubRelStr of b₃

proof end;

theorem Th15: :: WAYBEL10:15

for b₁ being complete LATTICE
for b₂, b₃ being closure Function of b₁,b₁ holds
( b₂ <= b₃ iff Image b₃ is SubRelStr of Image b₂ )

proof end;

definition

let c₁ be RelStr ;
func Sub c₁ -> non empty strict RelStr means :Def3: :: WAYBEL10:def 3
( ( for b₁ being set holds
( b₁ is Element of a₂ iff b₁ is strict SubRelStr of a₁ ) ) & ( for b₁, b₂ being Element of a₂ holds
( b₁ <= b₂ iff ex b₃ being RelStr st
( b₂ = b₃ & b₁ is SubRelStr of b₃ ) ) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def3 defines Sub WAYBEL10:def 3 :

theorem Th16: :: WAYBEL10:16

for b₁, b₂ being RelStr
for b₃, b₄ being Element of (Sub b₁) st b₄ = b₂ holds
( b₃ <= b₄ iff b₃ is SubRelStr of b₂ )

proof end;

registration

let c₁ be RelStr ;
cluster Sub a₁ -> non empty strict reflexive transitive antisymmetric ;
coherence

proof end;

end;

registration

let c₁ be RelStr ;
cluster Sub a₁ -> non empty strict reflexive transitive antisymmetric complete ;
coherence

proof end;

end;

registration

let c₁ be complete LATTICE;
cluster infs-inheriting -> non empty SubRelStr of a₁;
coherence

proof end;

cluster sups-inheriting -> non empty SubRelStr of a₁;
coherence

proof end;

end;

definition

let c₁ be RelStr ;
mode System of a₁ is full SubRelStr of a₁;

end;

notation

let c₁ be non empty RelStr ;
let c₂ be System of c₁;
synonym closure c₂ for infs-inheriting c₂;

end;

registration

let c₁ be non empty RelStr ;
cluster subrelstr ([#] a₁) -> infs-inheriting sups-inheriting ;
coherence

proof end;

end;

definition

let c₁ be non empty RelStr ;
func ClosureSystems c₁ -> non empty strict full SubRelStr of Sub a₁ means :Def4: :: WAYBEL10:def 4
for b₁ being strict SubRelStr of a₁ holds
( b₁ is Element of a₂ iff ( b₁ is closure & b₁ is full ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def4 defines ClosureSystems WAYBEL10:def 4 :

theorem Th17: :: WAYBEL10:17

for b₁ being non empty RelStr
for b₂ being set holds
( b₂ is Element of (ClosureSystems b₁) iff b₂ is strict closure System of b₁ )

proof end;

theorem Th18: :: WAYBEL10:18

for b₁ being non empty RelStr
for b₂ being RelStr
for b₃, b₄ being Element of (ClosureSystems b₁) st b₄ = b₂ holds
( b₃ <= b₄ iff b₃ is SubRelStr of b₂ )

proof end;

registration

let c₁ be non empty Poset;
let c₂ be closure Function of c₁,c₁;
cluster Image a₂ -> infs-inheriting ;
coherence by WAYBEL_1:56;

end;

definition

let c₁ be non empty Poset;
func ClImageMap c₁ -> Function of (ClOpers a₁),((ClosureSystems a₁) opp ) means :Def5: :: WAYBEL10:def 5
for b₁ being closure Function of a₁,a₁ holds a₂ . b₁ = Image b₁;
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def5 defines ClImageMap WAYBEL10:def 5 :

definition

let c₁ be non empty RelStr ;
let c₂ be SubRelStr of c₁;
func closure_op c₂ -> Function of a₁,a₁ means :Def6: :: WAYBEL10:def 6
for b₁ being Element of a₁ holds a₃ . b₁ = "/\" ((uparrow b₁) /\ the carrier of a₂),a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines closure_op WAYBEL10:def 6 :

registration

let c₁ be complete LATTICE;
let c₂ be closure System of c₁;
cluster closure_op a₂ -> idempotent monotone closure ;
coherence

proof end;

end;

theorem Th19: :: WAYBEL10:19

for b₁ being complete LATTICE
for b₂ being closure System of b₁ holds Image (closure_op b₂) = RelStr(# the carrier of b₂,the InternalRel of b₂ #)

proof end;

theorem Th20: :: WAYBEL10:20

for b₁ being complete LATTICE
for b₂ being closure Function of b₁,b₁ holds closure_op (Image b₂) = b₂

proof end;

registration

let c₁ be complete LATTICE;
cluster ClImageMap a₁ -> V5 ;
coherence

proof end;

end;

theorem Th21: :: WAYBEL10:21

for b₁ being complete LATTICE holds (ClImageMap b₁) " is Function of ((ClosureSystems b₁) opp ),(ClOpers b₁)

proof end;

theorem Th22: :: WAYBEL10:22

for b₁ being complete LATTICE
for b₂ being strict closure System of b₁ holds ((ClImageMap b₁) " ) . b₂ = closure_op b₂

proof end;

registration

let c₁ be complete LATTICE;
cluster ClImageMap a₁ -> V5 isomorphic ;
correctness

proof end;

end;

theorem Th23: :: WAYBEL10:23

for b₁ being complete LATTICE holds ClOpers b₁,(ClosureSystems b₁) opp are_isomorphic

proof end;

theorem Th24: :: WAYBEL10:24

for b₁ being RelStr
for b₂ being full SubRelStr of b₁
for b₃ being Subset of b₂ holds
( ( b₃ is directed Subset of b₁ implies b₃ is directed ) & ( b₃ is filtered Subset of b₁ implies b₃ is filtered ) )

proof end;

theorem Th25: :: WAYBEL10:25

for b₁ being complete LATTICE
for b₂ being closure System of b₁ holds
( closure_op b₂ is directed-sups-preserving iff b₂ is directed-sups-inheriting )

proof end;

theorem Th26: :: WAYBEL10:26

for b₁ being complete LATTICE
for b₂ being closure Function of b₁,b₁ holds
( b₂ is directed-sups-preserving iff Image b₂ is directed-sups-inheriting )

proof end;

registration

let c₁ be complete LATTICE;
let c₂ be closure directed-sups-inheriting System of c₁;
cluster closure_op a₂ -> idempotent monotone directed-sups-preserving closure ;
coherence by Th25;

end;

registration

let c₁ be complete LATTICE;
let c₂ be directed-sups-preserving closure Function of c₁,c₁;
cluster Image a₂ -> infs-inheriting directed-sups-inheriting ;
coherence

proof end;

end;

definition

let c₁ be non empty reflexive RelStr ;
func DsupClOpers c₁ -> non empty strict full SubRelStr of ClOpers a₁ means :Def7: :: WAYBEL10:def 7
for b₁ being closure Function of a₁,a₁ holds
( b₁ is Element of a₂ iff b₁ is directed-sups-preserving );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def7 defines DsupClOpers WAYBEL10:def 7 :

theorem Th27: :: WAYBEL10:27

for b₁ being non empty reflexive RelStr
for b₂ being set holds
( b₂ is Element of (DsupClOpers b₁) iff b₂ is directed-sups-preserving closure Function of b₁,b₁ )

proof end;

definition

let c₁ be non empty RelStr ;
func Subalgebras c₁ -> non empty strict full SubRelStr of ClosureSystems a₁ means :Def8: :: WAYBEL10:def 8
for b₁ being strict closure System of a₁ holds
( b₁ is Element of a₂ iff b₁ is directed-sups-inheriting );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def8 defines Subalgebras WAYBEL10:def 8 :

theorem Th28: :: WAYBEL10:28

for b₁ being non empty RelStr
for b₂ being set holds
( b₂ is Element of (Subalgebras b₁) iff b₂ is strict closure directed-sups-inheriting System of b₁ )

proof end;

theorem Th29: :: WAYBEL10:29

for b₁ being complete LATTICE holds Image ((ClImageMap b₁) | (DsupClOpers b₁)) = (Subalgebras b₁) opp

proof end;

registration

let c₁ be complete LATTICE;
cluster corestr ((ClImageMap a₁) | (DsupClOpers a₁)) -> monotone isomorphic ;
coherence

proof end;

end;

theorem Th30: :: WAYBEL10:30

for b₁ being complete LATTICE holds DsupClOpers b₁,(Subalgebras b₁) opp are_isomorphic

proof end;