begin
theorem Th1:
theorem
theorem
theorem Th4:
theorem
theorem
theorem Th7:
begin
:: deftheorem CLOSURE1:def 1 :
canceled;
:: deftheorem Def2 defines reflexive CLOSURE1:def 2 :
for I being set
for M being ManySortedSet of I
for IT being MSSetOp of M holds
( IT is reflexive iff for X being Element of bool M holds X c= IT .. X );
:: deftheorem Def3 defines monotonic CLOSURE1:def 3 :
for I being set
for M being ManySortedSet of I
for IT being MSSetOp 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 Def4 defines idempotent CLOSURE1:def 4 :
for I being set
for M being ManySortedSet of I
for IT being MSSetOp of M holds
( IT is idempotent iff for X being Element of bool M holds IT .. X = IT .. (IT .. X) );
:: deftheorem Def5 defines topological CLOSURE1:def 5 :
for I being set
for M being ManySortedSet of I
for IT being MSSetOp of M holds
( IT is topological iff for X, Y being Element of bool M holds IT .. (X \/ Y) = (IT .. X) \/ (IT .. Y) );
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem
begin
:: deftheorem Def6 defines additive CLOSURE1:def 6 :
for S being 1-sorted
for IT being MSClosureStr of S holds
( IT is additive iff the Family of IT is additive );
:: deftheorem Def7 defines absolutely-additive CLOSURE1:def 7 :
for S being 1-sorted
for IT being MSClosureStr of S holds
( IT is absolutely-additive iff the Family of IT is absolutely-additive );
:: deftheorem Def8 defines multiplicative CLOSURE1:def 8 :
for S being 1-sorted
for IT being MSClosureStr of S holds
( IT is multiplicative iff the Family of IT is multiplicative );
:: deftheorem Def9 defines absolutely-multiplicative CLOSURE1:def 9 :
for S being 1-sorted
for IT being MSClosureStr of S holds
( IT is absolutely-multiplicative iff the Family of IT is absolutely-multiplicative );
:: deftheorem Def10 defines properly-upper-bound CLOSURE1:def 10 :
for S being 1-sorted
for IT being MSClosureStr of S holds
( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );
:: deftheorem Def11 defines properly-lower-bound CLOSURE1:def 11 :
for S being 1-sorted
for IT being MSClosureStr of S holds
( IT is properly-lower-bound iff the Family of IT is properly-lower-bound );
:: deftheorem defines MSFull CLOSURE1:def 12 :
for S being 1-sorted
for MS being many-sorted of S holds MSFull MS = MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);
:: deftheorem Def13 defines MSFixPoints CLOSURE1:def 13 :
for I being set
for M being ManySortedSet of I
for F being ManySortedFunction of M,M
for b4 being ManySortedSubset of M holds
( b4 = MSFixPoints F iff for x, i being set st i in I holds
( x in b4 . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) );
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem Th37:
theorem
:: deftheorem Def14 defines ClOp->ClSys CLOSURE1:def 14 :
for S being 1-sorted
for A being ManySortedSet of the carrier of S
for C being MSClosureOperator of A
for b4 being MSClosureSystem of S holds
( b4 = ClOp->ClSys C iff ex D being MSSubsetFamily of A st
( D = MSFixPoints C & b4 = MSClosureStr(# A,D #) ) );
:: deftheorem Def15 defines ClSys->ClOp CLOSURE1:def 15 :
for S being 1-sorted
for D being MSClosureSystem of S
for b3 being MSClosureOperator of the Sorts of D holds
( b3 = ClSys->ClOp D iff for X being Element of bool the Sorts of D
for SF being V8() MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) ) holds
b3 .. X = meet SF );
theorem
theorem