:: WAYBEL10 semantic presentation

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

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

provided

A1: P₁[F₂()] and
A2: F₂() in the carrier of F₁()

proof end;

scheme :: WAYBEL10:sch 2
RelstrEq{ 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

A1: for x being set holds
( x is Element of F₁() iff P₁[x] ) and
A2: for x being set holds
( x is Element of F₂() iff P₁[x] ) and
A3: for a, b being Element of F₁() holds
( a <= b iff P₂[a,b] ) and
A4: for a, b being Element of F₂() holds
( a <= b iff P₂[a,b] )

proof end;

scheme :: WAYBEL10:sch 3
SubrelstrEq1{ 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

A1: for x being set holds
( x is Element of F₂() iff P₁[x] ) and
A2: for x being set holds
( x is Element of F₃() iff P₁[x] )

proof end;

scheme :: WAYBEL10:sch 4
SubrelstrEq2{ 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

A1: for x being Element of F₁() holds
( x is Element of F₂() iff P₁[x] ) and
A2: for x being Element of F₁() holds
( x is Element of F₃() iff P₁[x] )

proof end;

theorem Th1: :: WAYBEL10:1

for R, Q being Relation holds
( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) )

proof end;

theorem :: WAYBEL10:2

canceled;

theorem Th3: :: WAYBEL10:3

for L, S being RelStr holds
( ( S is SubRelStr of L implies S opp is SubRelStr of L opp ) & ( S opp is SubRelStr of L opp implies S is SubRelStr of L ) & ( S opp is SubRelStr of L implies S is SubRelStr of L opp ) & ( S is SubRelStr of L opp implies S opp is SubRelStr of L ) )

proof end;

theorem Th4: :: WAYBEL10:4

for L, S being RelStr holds
( ( S is full SubRelStr of L implies S opp is full SubRelStr of L opp ) & ( S opp is full SubRelStr of L opp implies S is full SubRelStr of L ) & ( S opp is full SubRelStr of L implies S is full SubRelStr of L opp ) & ( S is full SubRelStr of L opp implies S opp is full SubRelStr of L ) )

proof end;

definition

let L be RelStr ;
let S be full SubRelStr of L;
:: original: ~
redefine func S opp -> strict full SubRelStr of L opp ;
coherence by Th4;

end;

registration

let X be set ;
let L be non empty RelStr ;
cluster K104(X,L) -> non-Empty ;
coherence

proof end;

end;

registration

let S be RelStr ;
let T be non empty reflexive RelStr ;
cluster monotone Relation of the carrier of S,the carrier of T;
existence

proof end;

end;

registration

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

end;

registration

let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
cluster corestr f -> monotone ;
coherence

proof end;

end;

registration

let L be 1-sorted ;
cluster id L -> one-to-one ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem :: WAYBEL10:5

for L being RelStr
for S being Subset of L holds
( id S is Function of (subrelstr S),L & ( for f being Function of (subrelstr S),L st f = id S holds
f is monotone ) )

proof end;

registration

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

proof end;

end;

theorem Th6: :: WAYBEL10:6

for L being non empty reflexive RelStr
for c being closure Function of L,L
for x being Element of L holds c . x >= x

proof end;

definition

let S, T be 1-sorted ;
let f be Function of the carrier of S,the carrier of T;
let R be 1-sorted ;
assume A1: the carrier of R c= the carrier of S ;
func f | R -> Function of R,T equals :Def1: :: WAYBEL10:def 1
f | the carrier of R;
coherence

proof end;

correctness ;

end;

:: deftheorem Def1 defines | WAYBEL10:def 1 :

theorem Th7: :: WAYBEL10:7

for S, T being RelStr
for R being SubRelStr of S
for f being Function of the carrier of S,the carrier of T holds
( f | R = f | the carrier of R & ( for x being set st x in the carrier of R holds
(f | R) . x = f . x ) )

proof end;

theorem Th8: :: WAYBEL10:8

for S, T being RelStr
for f being Function of S,T st f is one-to-one holds
for R being SubRelStr of S holds f | R is one-to-one

proof end;

registration

let S, T be non empty reflexive RelStr ;
let f be monotone Function of S,T;
let R be SubRelStr of S;
cluster f | R -> monotone ;
coherence

proof end;

end;

theorem Th9: :: WAYBEL10:9

for S, T being non empty RelStr
for R being non empty SubRelStr of S
for f being Function of S,T
for g being Function of T,S st f is one-to-one & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )

proof end;

registration

let S be RelStr ;
let T be non empty reflexive RelStr ;
cluster MonMaps S,T -> non empty ;
coherence

proof end;

end;

theorem Th10: :: WAYBEL10:10

for S being RelStr
for T being non empty reflexive RelStr
for x being set holds
( x is Element of (MonMaps S,T) iff x is monotone Function of S,T )

proof end;

definition

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

proof end;

correctness

proof end;

end;

:: deftheorem Def2 defines ClOpers WAYBEL10:def 2 :

theorem Th11: :: WAYBEL10:11

for L being non empty reflexive RelStr
for x being set holds
( x is Element of (ClOpers L) iff x is closure Function of L,L )

proof end;

theorem Th12: :: WAYBEL10:12

for X being set
for L being non empty RelStr
for f, g being Function of X,the carrier of L
for x, y being Element of (L |^ X) st x = f & y = g holds
( x <= y iff f <= g )

proof end;

theorem Th13: :: WAYBEL10:13

for L being complete LATTICE
for c1, c2 being Function of L,L
for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds
( x <= y iff c1 <= c2 )

proof end;

theorem Th14: :: WAYBEL10:14

for L being reflexive RelStr
for S1, S2 being full SubRelStr of L st the carrier of S1 c= the carrier of S2 holds
S1 is SubRelStr of S2

proof end;

theorem Th15: :: WAYBEL10:15

for L being complete LATTICE
for c1, c2 being closure Function of L,L holds
( c1 <= c2 iff Image c2 is SubRelStr of Image c1 )

proof end;

definition

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

proof end;

correctness

proof end;

end;

:: deftheorem Def3 defines Sub WAYBEL10:def 3 :

theorem Th16: :: WAYBEL10:16

for L, R being RelStr
for x, y being Element of (Sub L) st y = R holds
( x <= y iff x is SubRelStr of R )

proof end;

registration

let L be RelStr ;
cluster Sub L -> non empty strict reflexive transitive antisymmetric ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let L be complete LATTICE;
cluster infs-inheriting -> non empty SubRelStr of L;
coherence

proof end;

cluster sups-inheriting -> non empty SubRelStr of L;
coherence

proof end;

end;

definition

let L be RelStr ;
mode System of L is full SubRelStr of L;

end;

notation

let L be non empty RelStr ;
let S be System of L;
synonym closure S for infs-inheriting S;

end;

registration

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

proof end;

end;

definition

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

proof end;

correctness

proof end;

end;

:: deftheorem Def4 defines ClosureSystems WAYBEL10:def 4 :

theorem Th17: :: WAYBEL10:17

for L being non empty RelStr
for x being set holds
( x is Element of (ClosureSystems L) iff x is strict closure System of L )

proof end;

theorem Th18: :: WAYBEL10:18

for L being non empty RelStr
for R being RelStr
for x, y being Element of (ClosureSystems L) st y = R holds
( x <= y iff x is SubRelStr of R )

proof end;

registration

let L be non empty Poset;
let h be closure Function of L,L;
cluster Image h -> infs-inheriting ;
coherence by WAYBEL_1:56;

end;

definition

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

proof end;

correctness

proof end;

end;

:: deftheorem Def5 defines ClImageMap WAYBEL10:def 5 :

definition

let L be non empty RelStr ;
let S be SubRelStr of L;
func closure_op S -> Function of L,L means :Def6: :: WAYBEL10:def 6
for x being Element of L holds it . x = "/\" ((uparrow x) /\ the carrier of S),L;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines closure_op WAYBEL10:def 6 :

registration

let L be complete LATTICE;
let S be closure System of L;
cluster closure_op S -> idempotent monotone closure ;
coherence

proof end;

end;

theorem Th19: :: WAYBEL10:19

for L being complete LATTICE
for S being closure System of L holds Image (closure_op S) = RelStr(# the carrier of S,the InternalRel of S #)

proof end;

theorem Th20: :: WAYBEL10:20

for L being complete LATTICE
for c being closure Function of L,L holds closure_op (Image c) = c

proof end;

registration

let L be complete LATTICE;
cluster ClImageMap L -> V5 ;
coherence

proof end;

end;

theorem Th21: :: WAYBEL10:21

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

proof end;

theorem Th22: :: WAYBEL10:22

for L being complete LATTICE
for S being strict closure System of L holds ((ClImageMap L) " ) . S = closure_op S

proof end;

registration

let L be complete LATTICE;
cluster ClImageMap L -> V5 isomorphic ;
correctness

proof end;

end;

theorem :: WAYBEL10:23

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

proof end;

theorem Th24: :: WAYBEL10:24

for L being RelStr
for S being full SubRelStr of L
for X being Subset of S holds
( ( X is directed Subset of L implies X is directed ) & ( X is filtered Subset of L implies X is filtered ) )

proof end;

theorem Th25: :: WAYBEL10:25

for L being complete LATTICE
for S being closure System of L holds
( closure_op S is directed-sups-preserving iff S is directed-sups-inheriting )

proof end;

theorem :: WAYBEL10:26

for L being complete LATTICE
for h being closure Function of L,L holds
( h is directed-sups-preserving iff Image h is directed-sups-inheriting )

proof end;

registration

let L be complete LATTICE;
let S be closure directed-sups-inheriting System of L;
cluster closure_op S -> idempotent monotone directed-sups-preserving closure ;
coherence by Th25;

end;

registration

let L be complete LATTICE;
let h be directed-sups-preserving closure Function of L,L;
cluster Image h -> infs-inheriting directed-sups-inheriting ;
coherence

proof end;

end;

definition

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

proof end;

correctness

proof end;

end;

:: deftheorem Def7 defines DsupClOpers WAYBEL10:def 7 :

theorem Th27: :: WAYBEL10:27

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

proof end;

definition

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

proof end;

correctness

proof end;

end;

:: deftheorem Def8 defines Subalgebras WAYBEL10:def 8 :

theorem Th28: :: WAYBEL10:28

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

proof end;

theorem Th29: :: WAYBEL10:29

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

proof end;

registration

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

proof end;

end;

theorem :: WAYBEL10:30

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

proof end;