:: On the Closure Operator and the Closure System of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received February 7, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

notation

let I be set ;
let A, B be ManySortedSet of I;
synonym A in' B for A in B;

end;

notation

let I be set ;
let A, B be ManySortedSet of I;
synonym A c=' B for A c= B;

end;

theorem :: CLOSURE2:1

for M being non empty set
for X, Y being Element of M st X c= Y holds
(id M) . X c= (id M) . Y ;

theorem Th2: :: CLOSURE2:2

for I being non empty set
for A being ManySortedSet of I
for B being ManySortedSubset of A holds rng B c= union (rng (bool A))

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
defpred S₁[ object ] means $1 is ManySortedSubset of M;

func Bool M -> set means :Def1: :: CLOSURE2:def 1
for x being object holds
( x in it iff x is ManySortedSubset of M );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff x is ManySortedSubset of M )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff x is ManySortedSubset of M ) ) & ( for x being object holds
( x in b₂ iff x is ManySortedSubset of M ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Bool CLOSURE2:def 1 :
for I being set
for M being ManySortedSet of I
for b₃ being set holds
( b₃ = Bool M iff for x being object holds
( x in b₃ iff x is ManySortedSubset of M ) );

registration

let I be set ;
let M be ManySortedSet of I;

cluster Bool M -> non empty functional with_common_domain ;

coherence
( not Bool M is empty & Bool M is functional & Bool M is with_common_domain )

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
mode SubsetFamily of M is Subset of (Bool M);

end;

definition

let I be set ;
let M be ManySortedSet of I;
:: original: Bool
redefine func Bool M -> SubsetFamily of M;
coherence
Bool M is SubsetFamily of M

proof end;

end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster non empty functional with_common_domain for Element of bool (Bool M);

existence
ex b₁ being SubsetFamily of M st
( not b₁ is empty & b₁ is functional & b₁ is with_common_domain )

proof end;

end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster empty functional finite for Element of bool (Bool M);

existence
ex b₁ being SubsetFamily of M st
( b₁ is empty & b₁ is finite )

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
let S be non empty SubsetFamily of M;
:: original: Element
redefine mode Element of S -> ManySortedSubset of M;
coherence
for b₁ being Element of S holds b₁ is ManySortedSubset of M

proof end;

end;

theorem Th3: :: CLOSURE2:3

for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF \/ SG is SubsetFamily of M ;

theorem :: CLOSURE2:4

for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF /\ SG is SubsetFamily of M ;

theorem :: CLOSURE2:5

for x, I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M holds SF \ x is SubsetFamily of M ;

theorem :: CLOSURE2:6

for I being set
for M being ManySortedSet of I
for SF, SG being SubsetFamily of M holds SF \+\ SG is SubsetFamily of M ;

theorem Th7: :: CLOSURE2:7

for I being set
for A, M being ManySortedSet of I st A c= M holds
{A} is SubsetFamily of M

proof end;

theorem Th8: :: CLOSURE2:8

for I being set
for A, B, M being ManySortedSet of I st A c= M & B c= M holds
{A,B} is SubsetFamily of M

proof end;

theorem Th9: :: CLOSURE2:9

for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E (/\) T in Bool M

proof end;

theorem Th10: :: CLOSURE2:10

for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E (\/) T in Bool M

proof end;

theorem :: CLOSURE2:11

for I being set
for A, M being ManySortedSet of I
for E being Element of Bool M holds E (\) A in Bool M

proof end;

theorem :: CLOSURE2:12

for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M holds E (\+\) T in Bool M

proof end;

:: to the Operator on Many Sorted Subsets

definition

let S be functional set ;

func |.S.| -> Function means :Def2: :: CLOSURE2:def 2
ex A being non empty functional set st
( A = S & dom it = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom it holds
it . i = { (x . i) where x is Element of A : verum } ) ) if S <> {}
otherwise it = {} ;

existence
( ( S <> {} implies ex b₁ being Function ex A being non empty functional set st
( A = S & dom b₁ = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b₁ holds
b₁ . i = { (x . i) where x is Element of A : verum } ) ) ) & ( not S <> {} implies ex b₁ being Function st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being Function holds
( ( S <> {} & ex A being non empty functional set st
( A = S & dom b₁ = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b₁ holds
b₁ . i = { (x . i) where x is Element of A : verum } ) ) & ex A being non empty functional set st
( A = S & dom b₂ = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b₂ holds
b₂ . i = { (x . i) where x is Element of A : verum } ) ) implies b₁ = b₂ ) & ( not S <> {} & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Function holds verum ;

end;

:: deftheorem Def2 defines |. CLOSURE2:def 2 :
for S being functional set
for b₂ being Function holds
( ( S <> {} implies ( b₂ = |.S.| iff ex A being non empty functional set st
( A = S & dom b₂ = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b₂ holds
b₂ . i = { (x . i) where x is Element of A : verum } ) ) ) ) & ( not S <> {} implies ( b₂ = |.S.| iff b₂ = {} ) ) );

theorem Th13: :: CLOSURE2:13

for I being set
for M being ManySortedSet of I
for SF being non empty SubsetFamily of M holds dom |.SF.| = I

proof end;

registration

let S be empty functional set ;

cluster |.S.| -> empty ;

coherence
|.S.| is empty by Def2;

end;

definition

let I be set ;
let M be ManySortedSet of I;
let S be SubsetFamily of M;

func |:S:| -> ManySortedSet of I equals :Def3: :: CLOSURE2:def 3
|.S.| if S <> {}
otherwise EmptyMS I;

coherence
( ( S <> {} implies |.S.| is ManySortedSet of I ) & ( not S <> {} implies EmptyMS I is ManySortedSet of I ) )

proof end;

consistency
for b₁ being ManySortedSet of I holds verum ;

end;

:: deftheorem Def3 defines |: CLOSURE2:def 3 :
for I being set
for M being ManySortedSet of I
for S being SubsetFamily of M holds
( ( S <> {} implies |:S:| = |.S.| ) & ( not S <> {} implies |:S:| = EmptyMS I ) );

registration

let I be set ;
let M be ManySortedSet of I;
let S be empty SubsetFamily of M;

cluster |:S:| -> V9() ;

coherence
|:S:| is empty-yielding

proof end;

end;

theorem Th14: :: CLOSURE2:14

for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }

proof end;

registration

let I be set ;
let M be ManySortedSet of I;
let SF be non empty SubsetFamily of M;

cluster |:SF:| -> V8() ;

coherence
|:SF:| is non-empty

proof end;

end;

theorem Th15: :: CLOSURE2:15

for f being Function holds dom |.{f}.| = dom f

proof end;

theorem :: CLOSURE2:16

for f, f1 being Function holds dom |.{f,f1}.| = (dom f) /\ (dom f1)

proof end;

theorem Th17: :: CLOSURE2:17

for i being set
for f being Function st i in dom f holds
|.{f}.| . i = {(f . i)}

proof end;

theorem :: CLOSURE2:18

for i, I being set
for M being ManySortedSet of I
for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}

proof end;

theorem Th19: :: CLOSURE2:19

for i being set
for f, f1 being Function st i in dom |.{f,f1}.| holds
|.{f,f1}.| . i = {(f . i),(f1 . i)}

proof end;

theorem Th20: :: CLOSURE2:20

for i, I being set
for M being ManySortedSet of I
for f, f1 being Function
for SF being SubsetFamily of M st i in I & SF = {f,f1} holds
|:SF:| . i = {(f . i),(f1 . i)}

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let SF be SubsetFamily of M;
:: original: |:
redefine func |:SF:| -> MSSubsetFamily of M;
coherence
|:SF:| is MSSubsetFamily of M

proof end;

end;

theorem Th21: :: CLOSURE2:21

for I being set
for A, M being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|

proof end;

theorem Th22: :: CLOSURE2:22

for I being set
for A, B, M being ManySortedSet of I
for SF being SubsetFamily of M st SF = {A,B} holds
union |:SF:| = A (\/) B

proof end;

theorem Th23: :: CLOSURE2:23

for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E (/\) T

proof end;

theorem Th24: :: CLOSURE2:24

for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|

proof end;

theorem :: CLOSURE2:25

for I being set
for M being ManySortedSet of I holds |:(Bool M):| = bool M

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let IT be SubsetFamily of M;

attr IT is additive means :: CLOSURE2:def 4
for A, B being ManySortedSet of I st A in IT & B in IT holds
A (\/) B in IT;

attr IT is absolutely-additive means :: CLOSURE2:def 5
for F being SubsetFamily of M st F c= IT holds
union |:F:| in IT;

attr IT is multiplicative means :: CLOSURE2:def 6
for A, B being ManySortedSet of I st A in IT & B in IT holds
A (/\) B in IT;

attr IT is absolutely-multiplicative means :Def7: :: CLOSURE2:def 7
for F being SubsetFamily of M st F c= IT holds
meet |:F:| in IT;

attr IT is properly-upper-bound means :Def8: :: CLOSURE2:def 8
M in IT;

attr IT is properly-lower-bound means :: CLOSURE2:def 9
EmptyMS I in IT;

end;

:: deftheorem defines additive CLOSURE2:def 4 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is additive iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A (\/) B in IT );

:: deftheorem defines absolutely-additive CLOSURE2:def 5 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is absolutely-additive iff for F being SubsetFamily of M st F c= IT holds
union |:F:| in IT );

:: deftheorem defines multiplicative CLOSURE2:def 6 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is multiplicative iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A (/\) B in IT );

:: deftheorem Def7 defines absolutely-multiplicative CLOSURE2:def 7 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is absolutely-multiplicative iff for F being SubsetFamily of M st F c= IT holds
meet |:F:| in IT );

:: deftheorem Def8 defines properly-upper-bound CLOSURE2:def 8 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is properly-upper-bound iff M in IT );

:: deftheorem defines properly-lower-bound CLOSURE2:def 9 :
for I being set
for M being ManySortedSet of I
for IT being SubsetFamily of M holds
( IT is properly-lower-bound iff EmptyMS I in IT );

Lm1: for I being set
for M being ManySortedSet of I holds
( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound )

proof end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for Element of bool (Bool M);

existence
ex b₁ being SubsetFamily of M st
( not b₁ is empty & b₁ is functional & b₁ is with_common_domain & b₁ is additive & b₁ is absolutely-additive & b₁ is multiplicative & b₁ is absolutely-multiplicative & b₁ is properly-upper-bound & b₁ is properly-lower-bound )

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
:: original: Bool
redefine func Bool M -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M;
coherence
Bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M by Lm1;

end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster absolutely-additive -> additive for Element of bool (Bool M);

coherence
for b₁ being SubsetFamily of M st b₁ is absolutely-additive holds
b₁ is additive

proof end;

end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster absolutely-multiplicative -> multiplicative for Element of bool (Bool M);

coherence
for b₁ being SubsetFamily of M st b₁ is absolutely-multiplicative holds
b₁ is multiplicative

proof end;

end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster absolutely-multiplicative -> properly-upper-bound for Element of bool (Bool M);

coherence
for b₁ being SubsetFamily of M st b₁ is absolutely-multiplicative holds
b₁ is properly-upper-bound

proof end;

end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster properly-upper-bound -> non empty for Element of bool (Bool M);

coherence
for b₁ being SubsetFamily of M st b₁ is properly-upper-bound holds
not b₁ is empty ;

end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster absolutely-additive -> properly-lower-bound for Element of bool (Bool M);

coherence
for b₁ being SubsetFamily of M st b₁ is absolutely-additive holds
b₁ is properly-lower-bound

proof end;

end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster properly-lower-bound -> non empty for Element of bool (Bool M);

coherence
for b₁ being SubsetFamily of M st b₁ is properly-lower-bound holds
not b₁ is empty ;

end;

definition

let I be set ;
let M be ManySortedSet of I;
mode SetOp of M is Function of (Bool M),(Bool M);

end;

definition

let I be set ;
let M be ManySortedSet of I;
let f be SetOp of M;
let x be Element of Bool M;
:: original: .
redefine func f . x -> Element of Bool M;
coherence
f . x is Element of Bool M

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
let IT be SetOp of M;

attr IT is reflexive means :Def10: :: CLOSURE2:def 10
for x being Element of Bool M holds x c=' IT . x;

attr IT is monotonic means :Def11: :: CLOSURE2:def 11
for x, y being Element of Bool M st x c=' y holds
IT . x c=' IT . y;

attr IT is idempotent means :Def12: :: CLOSURE2:def 12
for x being Element of Bool M holds IT . x = IT . (IT . x);

attr IT is topological means :: CLOSURE2:def 13
for x, y being Element of Bool M holds IT . (x (\/) y) = (IT . x) (\/) (IT . y);

end;

:: deftheorem Def10 defines reflexive CLOSURE2:def 10 :
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is reflexive iff for x being Element of Bool M holds x c=' IT . x );

:: deftheorem Def11 defines monotonic CLOSURE2:def 11 :
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is monotonic iff for x, y being Element of Bool M st x c=' y holds
IT . x c=' IT . y );

:: deftheorem Def12 defines idempotent CLOSURE2:def 12 :
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is idempotent iff for x being Element of Bool M holds IT . x = IT . (IT . x) );

:: deftheorem defines topological CLOSURE2:def 13 :
for I being set
for M being ManySortedSet of I
for IT being SetOp of M holds
( IT is topological iff for x, y being Element of Bool M holds IT . (x (\/) y) = (IT . x) (\/) (IT . y) );

registration

let I be set ;
let M be ManySortedSet of I;

cluster non empty Relation-like Function-like V17( Bool M) quasi_total reflexive monotonic idempotent topological for Element of bool [:(Bool M),(Bool M):];

existence
ex b₁ being SetOp of M st
( b₁ is reflexive & b₁ is monotonic & b₁ is idempotent & b₁ is topological )

proof end;

end;

theorem :: CLOSURE2:26

for I being set
for A being ManySortedSet of I holds id (Bool A) is reflexive SetOp of A

proof end;

theorem :: CLOSURE2:27

for I being set
for A being ManySortedSet of I holds id (Bool A) is monotonic SetOp of A

proof end;

theorem :: CLOSURE2:28

for I being set
for A being ManySortedSet of I holds id (Bool A) is idempotent SetOp of A

proof end;

theorem :: CLOSURE2:29

for I being set
for A being ManySortedSet of I holds id (Bool A) is topological SetOp of A

proof end;

theorem :: CLOSURE2:30

for I being set
for M being ManySortedSet of I
for E being Element of Bool M
for g being SetOp of M st E = M & g is reflexive holds
E = g . E

proof end;

theorem :: CLOSURE2:31

for I being set
for M being ManySortedSet of I
for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds
g is idempotent

proof end;

theorem :: CLOSURE2:32

for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E (/\) T & g is monotonic holds
g . A c= (g . E) (/\) (g . T)

proof end;

registration

let I be set ;
let M be ManySortedSet of I;

cluster Function-like quasi_total topological -> monotonic for Element of bool [:(Bool M),(Bool M):];

coherence
for b₁ being SetOp of M st b₁ is topological holds
b₁ is monotonic

proof end;

end;

theorem :: CLOSURE2:33

for I being set
for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E (\) T & g is topological holds
(g . E) (\) (g . T) c= g . A

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let h, g be SetOp of M;
:: original: *
redefine func g * h -> SetOp of M;
coherence
h * g is SetOp of M

proof end;

end;

theorem :: CLOSURE2:34

for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is reflexive & h is reflexive holds
g * h is reflexive

proof end;

theorem :: CLOSURE2:35

for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is monotonic & h is monotonic holds
g * h is monotonic

proof end;

theorem :: CLOSURE2:36

for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds
g * h is idempotent

proof end;

theorem :: CLOSURE2:37

for I being set
for M being ManySortedSet of I
for g, h being SetOp of M st g is topological & h is topological holds
g * h is topological

proof end;

definition

let S be 1-sorted ;
attr c₂ is strict ;
struct ClosureStr over S -> many-sorted over S;
aggr ClosureStr(# Sorts, Family #) -> ClosureStr over S;
sel Family c₂ -> SubsetFamily of the Sorts of c₂;

end;

definition

let S be 1-sorted ;
let IT be ClosureStr over S;

attr IT is additive means :Def14: :: CLOSURE2:def 14
the Family of IT is additive ;

attr IT is absolutely-additive means :Def15: :: CLOSURE2:def 15
the Family of IT is absolutely-additive ;

attr IT is multiplicative means :Def16: :: CLOSURE2:def 16
the Family of IT is multiplicative ;

attr IT is absolutely-multiplicative means :Def17: :: CLOSURE2:def 17
the Family of IT is absolutely-multiplicative ;

attr IT is properly-upper-bound means :Def18: :: CLOSURE2:def 18
the Family of IT is properly-upper-bound ;

attr IT is properly-lower-bound means :Def19: :: CLOSURE2:def 19
the Family of IT is properly-lower-bound ;

end;

:: deftheorem Def14 defines additive CLOSURE2:def 14 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is additive iff the Family of IT is additive );

:: deftheorem Def15 defines absolutely-additive CLOSURE2:def 15 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is absolutely-additive iff the Family of IT is absolutely-additive );

:: deftheorem Def16 defines multiplicative CLOSURE2:def 16 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is multiplicative iff the Family of IT is multiplicative );

:: deftheorem Def17 defines absolutely-multiplicative CLOSURE2:def 17 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is absolutely-multiplicative iff the Family of IT is absolutely-multiplicative );

:: deftheorem Def18 defines properly-upper-bound CLOSURE2:def 18 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );

:: deftheorem Def19 defines properly-lower-bound CLOSURE2:def 19 :
for S being 1-sorted
for IT being ClosureStr over S holds
( IT is properly-lower-bound iff the Family of IT is properly-lower-bound );

definition

let S be 1-sorted ;
let MS be many-sorted over S;

func Full MS -> ClosureStr over S equals :: CLOSURE2:def 20
ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #);

correctness
coherence
ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #) is ClosureStr over S;
;

end;

:: deftheorem defines Full CLOSURE2:def 20 :
for S being 1-sorted
for MS being many-sorted over S holds Full MS = ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #);

registration

let S be 1-sorted ;
let MS be many-sorted over S;

cluster Full MS -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;

coherence
( Full MS is strict & Full MS is additive & Full MS is absolutely-additive & Full MS is multiplicative & Full MS is absolutely-multiplicative & Full MS is properly-upper-bound & Full MS is properly-lower-bound ) ;

end;

registration

let S be 1-sorted ;
let MS be non-empty many-sorted over S;

cluster Full MS -> non-empty ;

coherence
Full MS is non-empty ;

end;

registration

let S be 1-sorted ;

cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ClosureStr over S;

existence
ex b₁ being ClosureStr over S st
( b₁ is strict & b₁ is non-empty & b₁ is additive & b₁ is absolutely-additive & b₁ is multiplicative & b₁ is absolutely-multiplicative & b₁ is properly-upper-bound & b₁ is properly-lower-bound )

proof end;

end;

registration

let S be 1-sorted ;
let CS be additive ClosureStr over S;

cluster the Family of CS -> additive ;

coherence
the Family of CS is additive by Def14;

end;

registration

let S be 1-sorted ;
let CS be absolutely-additive ClosureStr over S;

cluster the Family of CS -> absolutely-additive ;

coherence
the Family of CS is absolutely-additive by Def15;

end;

registration

let S be 1-sorted ;
let CS be multiplicative ClosureStr over S;

cluster the Family of CS -> multiplicative ;

coherence
the Family of CS is multiplicative by Def16;

end;

registration

let S be 1-sorted ;
let CS be absolutely-multiplicative ClosureStr over S;

cluster the Family of CS -> absolutely-multiplicative ;

coherence
the Family of CS is absolutely-multiplicative by Def17;

end;

registration

let S be 1-sorted ;
let CS be properly-upper-bound ClosureStr over S;

cluster the Family of CS -> properly-upper-bound ;

coherence
the Family of CS is properly-upper-bound by Def18;

end;

registration

let S be 1-sorted ;
let CS be properly-lower-bound ClosureStr over S;

cluster the Family of CS -> properly-lower-bound ;

coherence
the Family of CS is properly-lower-bound by Def19;

end;

registration

let S be 1-sorted ;
let M be V8() ManySortedSet of the carrier of S;
let F be SubsetFamily of M;

cluster ClosureStr(# M,F #) -> non-empty ;

coherence
ClosureStr(# M,F #) is non-empty ;

end;

registration

let S be 1-sorted ;
let MS be many-sorted over S;
let F be additive SubsetFamily of the Sorts of MS;

cluster ClosureStr(# the Sorts of MS,F #) -> additive ;

coherence
ClosureStr(# the Sorts of MS,F #) is additive ;

end;

registration

let S be 1-sorted ;
let MS be many-sorted over S;
let F be absolutely-additive SubsetFamily of the Sorts of MS;

cluster ClosureStr(# the Sorts of MS,F #) -> absolutely-additive ;

coherence
ClosureStr(# the Sorts of MS,F #) is absolutely-additive ;

end;

registration

let S be 1-sorted ;
let MS be many-sorted over S;
let F be multiplicative SubsetFamily of the Sorts of MS;

cluster ClosureStr(# the Sorts of MS,F #) -> multiplicative ;

coherence
ClosureStr(# the Sorts of MS,F #) is multiplicative ;

end;

registration

let S be 1-sorted ;
let MS be many-sorted over S;
let F be absolutely-multiplicative SubsetFamily of the Sorts of MS;

cluster ClosureStr(# the Sorts of MS,F #) -> absolutely-multiplicative ;

coherence
ClosureStr(# the Sorts of MS,F #) is absolutely-multiplicative ;

end;

registration

let S be 1-sorted ;
let MS be many-sorted over S;
let F be properly-upper-bound SubsetFamily of the Sorts of MS;

cluster ClosureStr(# the Sorts of MS,F #) -> properly-upper-bound ;

coherence
ClosureStr(# the Sorts of MS,F #) is properly-upper-bound ;

end;

registration

let S be 1-sorted ;
let MS be many-sorted over S;
let F be properly-lower-bound SubsetFamily of the Sorts of MS;

cluster ClosureStr(# the Sorts of MS,F #) -> properly-lower-bound ;

coherence
ClosureStr(# the Sorts of MS,F #) is properly-lower-bound ;

end;

registration

let S be 1-sorted ;

cluster absolutely-additive -> additive for ClosureStr over S;

coherence
for b₁ being ClosureStr over S st b₁ is absolutely-additive holds
b₁ is additive ;

end;

registration

let S be 1-sorted ;

cluster absolutely-multiplicative -> multiplicative for ClosureStr over S;

coherence
for b₁ being ClosureStr over S st b₁ is absolutely-multiplicative holds
b₁ is multiplicative ;

end;

registration

let S be 1-sorted ;

cluster absolutely-multiplicative -> properly-upper-bound for ClosureStr over S;

coherence
for b₁ being ClosureStr over S st b₁ is absolutely-multiplicative holds
b₁ is properly-upper-bound ;

end;

registration

let S be 1-sorted ;

cluster absolutely-additive -> properly-lower-bound for ClosureStr over S;

coherence
for b₁ being ClosureStr over S st b₁ is absolutely-additive holds
b₁ is properly-lower-bound ;

end;

definition

let S be 1-sorted ;
mode ClosureSystem of S is absolutely-multiplicative ClosureStr over S;

end;

definition

let I be set ;
let M be ManySortedSet of I;
mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M;

end;

definition

let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;

func ClOp->ClSys g -> strict ClosureStr over S means :Def21: :: CLOSURE2:def 21
( the Sorts of it = A & the Family of it = { x where x is Element of Bool A : g . x = x } );

existence
ex b₁ being strict ClosureStr over S st
( the Sorts of b₁ = A & the Family of b₁ = { x where x is Element of Bool A : g . x = x } )

proof end;

uniqueness
for b₁, b₂ being strict ClosureStr over S st the Sorts of b₁ = A & the Family of b₁ = { x where x is Element of Bool A : g . x = x } & the Sorts of b₂ = A & the Family of b₂ = { x where x is Element of Bool A : g . x = x } holds
b₁ = b₂ ;

end;

:: deftheorem Def21 defines ClOp->ClSys CLOSURE2:def 21 :
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for g being ClosureOperator of A
for b₄ being strict ClosureStr over S holds
( b₄ = ClOp->ClSys g iff ( the Sorts of b₄ = A & the Family of b₄ = { x where x is Element of Bool A : g . x = x } ) );

registration

let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;

cluster ClOp->ClSys g -> strict absolutely-multiplicative ;

coherence
ClOp->ClSys g is absolutely-multiplicative

proof end;

end;

definition

let S be 1-sorted ;
let A be ClosureSystem of S;
let C be ManySortedSubset of the Sorts of A;

func Cl C -> Element of Bool the Sorts of A means :Def22: :: CLOSURE2:def 22
ex F being SubsetFamily of the Sorts of A st
( it = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } );

existence
ex b₁ being Element of Bool the Sorts of A ex F being SubsetFamily of the Sorts of A st
( b₁ = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } )

proof end;

uniqueness
for b₁, b₂ being Element of Bool the Sorts of A st ex F being SubsetFamily of the Sorts of A st
( b₁ = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) & ex F being SubsetFamily of the Sorts of A st
( b₂ = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) holds
b₁ = b₂ ;

end;

:: deftheorem Def22 defines Cl CLOSURE2:def 22 :
for S being 1-sorted
for A being ClosureSystem of S
for C being ManySortedSubset of the Sorts of A
for b₄ being Element of Bool the Sorts of A holds
( b₄ = Cl C iff ex F being SubsetFamily of the Sorts of A st
( b₄ = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) );

theorem Th38: :: CLOSURE2:38

for S being 1-sorted
for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st a in the Family of D & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
f . a = a

proof end;

theorem :: CLOSURE2:39

for S being 1-sorted
for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st f . a = a & ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
a in the Family of D

proof end;

theorem Th40: :: CLOSURE2:40

for S being 1-sorted
for D being ClosureSystem of S
for f being SetOp of the Sorts of D st ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
( f is reflexive & f is monotonic & f is idempotent )

proof end;

definition

let S be 1-sorted ;
let D be ClosureSystem of S;

func ClSys->ClOp D -> ClosureOperator of the Sorts of D means :Def23: :: CLOSURE2:def 23
for x being Element of Bool the Sorts of D holds it . x = Cl x;

existence
ex b₁ being ClosureOperator of the Sorts of D st
for x being Element of Bool the Sorts of D holds b₁ . x = Cl x

proof end;

uniqueness
for b₁, b₂ being ClosureOperator of the Sorts of D st ( for x being Element of Bool the Sorts of D holds b₁ . x = Cl x ) & ( for x being Element of Bool the Sorts of D holds b₂ . x = Cl x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def23 defines ClSys->ClOp CLOSURE2:def 23 :
for S being 1-sorted
for D being ClosureSystem of S
for b₃ being ClosureOperator of the Sorts of D holds
( b₃ = ClSys->ClOp D iff for x being Element of Bool the Sorts of D holds b₃ . x = Cl x );

theorem :: CLOSURE2:41

for S being 1-sorted
for A being ManySortedSet of the carrier of S
for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f

proof end;

deffunc H₁( set ) -> set = $1;

theorem :: CLOSURE2:42

for S being 1-sorted
for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)

proof end;