:: Algebraic Operation on Subsets of Many Sorted Sets
:: by Agnieszka Julia Marasik
::
:: Received June 23, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

registration
let S be non empty 1-sorted ;
cluster 1-sorted(# the carrier of S #) ->  non empty ;
coherence
 not 1-sorted(# the carrier of S #) is empty ;
end;

theorem Th1: :: CLOSURE3:1
for I being non empty set
for M, N being ManySortedSet of I holds M +* N = N
proofend;

theorem :: CLOSURE3:2
for I being set
for M, N being ManySortedSet of I
for F being SubsetFamily of M st N in F holds
meet |:F:| c=' N by CLOSURE2:21, MSSUBFAM:43;

theorem Th3: :: CLOSURE3:3
for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra over S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
proofend;

begin

theorem :: CLOSURE3:4
for A, B, C being set st A is_coarser_than B & B is_coarser_than C holds
A is_coarser_than C
proofend;

LM: now__::_thesis:_for_I_being_non_empty_set_
for_M_being_ManySortedSet_of_I_holds_support_M_=__{__x_where_x_is_Element_of_I_:_M_._x_<>_{}__}_
let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds support M =  {  x where x is Element of I : M . x <> {}  }
let M be ManySortedSet of I; ::_thesis: support M =  {  x where x is Element of I : M . x <> {}  }
set F =  {  x where x is Element of I : M . x <> {}  }  ;
thus  support M =  {  x where x is Element of I : M . x <> {}  }  ::_thesis: verum
proof
thus  support M c=  {  x where x is Element of I : M . x <> {}  }  :: according toXBOOLE_0:def_10 ::_thesis:  {  x where x is Element of I : M . x <> {}  }  c= support M
proof
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in support M or x in  {  x where x is Element of I : M . x <> {}  }  )
A1: dom M = I by PARTFUN1:def_2;
A2: support M c= dom M by PRE_POLY:37;
assume A3: x in support M ; ::_thesis: x in  {  x where x is Element of I : M . x <> {}  }
then  M . x <> {} by PRE_POLY:def_7;
hence  x in  {  x where x is Element of I : M . x <> {}  }  by A1, A2, A3; ::_thesis: verum
end;
let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in  {  x where x is Element of I : M . x <> {}  }  or x in support M )
assume  x in  {  x where x is Element of I : M . x <> {}  }  ; ::_thesis: x in support M
then  ex i being Element of I st
( x = i &amp; M . i <> {} ) ;
hence  x in support M by PRE_POLY:def_7; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let M be ManySortedSet of I;
:: original:support
redefine func support M ->  set  equals :: CLOSURE3:def 1
 {  x where x is Element of I : M . x <> {}  }  ;
compatibility
 for b1 being set holds
( b1 = support M iff b1 =  {  x where x is Element of I : M . x <> {}  }  ) by LM;
end;

:: deftheorem  defines support CLOSURE3:def_1_:_
 for I being non empty set
for M being ManySortedSet of I holds support M =  {  x where x is Element of I : M . x <> {}  }  ;

theorem :: CLOSURE3:5
for I being non empty set
for M being V8() ManySortedSet of I holds M = ([[0]] I) +* (M | (support M))
proofend;

theorem :: CLOSURE3:6
for I being non empty set
for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds
M1 = M2
proofend;

theorem :: CLOSURE3:7
canceled;

theorem Th8: :: CLOSURE3:8
for I being non empty set
for M being ManySortedSet of I
for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i &amp; a is V42() &amp; support a is finite &amp; a c= x )
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
let A be SubsetFamily of M;
func MSUnion A ->  ManySortedSubset of M means :Def2: :: CLOSURE3:def 2
 for i being set st i in I holds
it . i = union  {  (f . i) where f is Element of Bool M : f in A  }  ;
existence
 ex b1 being ManySortedSubset of M st
for i being set st i in I holds
b1 . i = union  {  (f . i) where f is Element of Bool M : f in A  }
proofend;
uniqueness
 for b1, b2 being ManySortedSubset of M st ( for i being set st i in I holds
b1 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  ) &amp; ( for i being set st i in I holds
b2 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines MSUnion CLOSURE3:def_2_:_
 for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M
for b4 being ManySortedSubset of M holds
( b4 = MSUnion A iff for i being set st i in I holds
b4 . i = union  {  (f . i) where f is Element of Bool M : f in A  }  );

registration
let I be set ;
let M be ManySortedSet of I;
let A be empty SubsetFamily of M;
cluster MSUnion A -> V9() ;
coherence
 MSUnion A is empty-yielding
proofend;
end;

theorem :: CLOSURE3:9
for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original:\/
redefine funcA \/ B ->  SubsetFamily of M;
correctness
coherence
A \/ B is SubsetFamily of M;
by CLOSURE2:3;
end;

theorem :: CLOSURE3:10
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
proofend;

theorem :: CLOSURE3:11
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original:/\
redefine funcA /\ B ->  SubsetFamily of M;
correctness
coherence
A /\ B is SubsetFamily of M;
by CLOSURE2:4;
end;

theorem :: CLOSURE3:12
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
proofend;

theorem :: CLOSURE3:13
for I being set
for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B =  {  (MSUnion X) where X is SubsetFamily of M : X in AA  }  &amp; A = union AA holds
MSUnion B = MSUnion A
proofend;

begin

definition
let I be non empty set ;
let M be ManySortedSet of I;
let S be SetOp of M;
attrS is algebraic  means :: CLOSURE3:def 3
 for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A =  {  (S . a) where a is Element of Bool M : ( a is V42() &amp; support a is finite &amp; a c= x )  }  &amp; x = MSUnion A );
end;

:: deftheorem  defines algebraic CLOSURE3:def_3_:_
 for I being non empty set
for M being ManySortedSet of I
for S being SetOp of M holds
( S is algebraic iff for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A =  {  (S . a) where a is Element of Bool M : ( a is V42() &amp; support a is finite &amp; a c= x )  }  &amp; x = MSUnion A ) );

registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster non empty Relation-like Bool M -defined Bool M -valued Function-like V17( Bool M) quasi_total reflexive monotonic idempotent algebraic for Element of bool [:(Bool M),(Bool M):];
existence
 ex b1 being SetOp of M st
( b1 is algebraic &amp; b1 is reflexive &amp; b1 is monotonic &amp; b1 is idempotent )
proofend;
end;

definition
let S be non empty 1-sorted ;
let IT be ClosureSystem of S;
attrIT is algebraic  means :: CLOSURE3:def 4
 ClSys->ClOp IT is algebraic ;
end;

:: deftheorem  defines algebraic CLOSURE3:def_4_:_
 for S being non empty 1-sorted
for IT being ClosureSystem of S holds
( IT is algebraic iff ClSys->ClOp IT is algebraic );

definition
let S be non empty non void ManySortedSign ;
let MA be non-empty MSAlgebra over S;
func SubAlgCl MA ->  strict ClosureStr over 1-sorted(# the carrier of S #) means :Def5: :: CLOSURE3:def 5
( the Sorts of it = the Sorts of MA &amp; the Family of it = SubSort MA );
existence
 ex b1 being strict ClosureStr over 1-sorted(# the carrier of S #) st
( the Sorts of b1 = the Sorts of MA &amp; the Family of b1 = SubSort MA )
proofend;
uniqueness
 for b1, b2 being strict ClosureStr over 1-sorted(# the carrier of S #) st the Sorts of b1 = the Sorts of MA &amp; the Family of b1 = SubSort MA &amp; the Sorts of b2 = the Sorts of MA &amp; the Family of b2 = SubSort MA holds
b1 = b2 ;
end;

:: deftheorem Def5 defines SubAlgCl CLOSURE3:def_5_:_
 for S being non empty non void ManySortedSign
for MA being non-empty MSAlgebra over S
for b3 being strict ClosureStr over 1-sorted(# the carrier of S #) holds
( b3 = SubAlgCl MA iff ( the Sorts of b3 = the Sorts of MA &amp; the Family of b3 = SubSort MA ) );

theorem Th14: :: CLOSURE3:14
for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
proofend;

registration
let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra over S;
cluster SubAlgCl MA ->  strict absolutely-multiplicative ;
coherence
 SubAlgCl MA is absolutely-multiplicative
proofend;
end;

registration
let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra over S;
cluster SubAlgCl MA ->  strict algebraic ;
coherence
 SubAlgCl MA is algebraic
proofend;
end;