Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Algebraic Operation on Subsets of Many Sorted Sets

**by****Agnieszka Julia Marasik**- Received June 23, 1997
- MML identifier: CLOSURE3

- [ Mizar article, MML identifier index ]

environ vocabulary PBOOLE, FUNCT_4, RELAT_1, CLOSURE2, SETFAM_1, MSSUBFAM, AMI_1, MSUALG_1, ZF_REFLE, MSUALG_2, UNIALG_2, BOOLE, CAT_4, FUNCT_1, QC_LANG1, TDGROUP, CANTOR_1, PRE_CIRC, FINSET_1, FUNCOP_1, TARSKI, MATRIX_1, WAYBEL_8, RELAT_2, MSAFREE2, BINOP_1, CLOSURE1, PROB_1, FUNCT_2, CLOSURE3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CANTOR_1, SETFAM_1, RELAT_1, FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, FINSET_1, FUNCT_4, PBOOLE, MSUALG_1, MSUALG_2, PROB_1, CLOSURE2, MSSUBFAM, MBOOLEAN, PRE_CIRC; constructors CLOSURE2, PRE_CIRC, PRALG_2, CANTOR_1, PROB_1, MSSUBFAM; clusters STRUCT_0, MSUALG_1, FUNCT_1, PBOOLE, CLOSURE2, FINSET_1, MSSUBFAM, RELSET_1, SUBSET_1, FUNCT_2, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries definition let S be non empty 1-sorted; cluster the 1-sorted of S -> non empty; end; theorem :: CLOSURE3:1 for I be non empty set, M, N be ManySortedSet of I holds M +* N = N; theorem :: CLOSURE3:2 for I be set, M, N be ManySortedSet of I, F be SubsetFamily of M holds N in F implies meet |:F:| c=' N; theorem :: CLOSURE3:3 for S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S for F be SubsetFamily of the Sorts of MA st F c= SubSort MA for B be MSSubset of MA st B = meet |:F:| holds B is opers_closed; begin :: Relationships between Subsets Families definition let I be set, M be ManySortedSet of I, B be SubsetFamily of M, A be SubsetFamily of M; pred A is_finer_than B means :: CLOSURE3:def 1 for a be set st a in A ex b be set st b in B & a c= b; reflexivity; pred B is_coarser_than A means :: CLOSURE3:def 2 for b be set st b in B ex a be set st a in A & a c= b; reflexivity; end; theorem :: CLOSURE3:4 for I be set, M be ManySortedSet of I for A,B,C be SubsetFamily of M holds A is_finer_than B & B is_finer_than C implies A is_finer_than C; theorem :: CLOSURE3:5 for I be set, M be ManySortedSet of I for A,B,C be SubsetFamily of M holds A is_coarser_than B & B is_coarser_than C implies A is_coarser_than C; definition let I be non empty set, M be ManySortedSet of I; func supp M -> set means :: CLOSURE3:def 3 it = { x where x is Element of I : M.x <> {} }; end; theorem :: CLOSURE3:6 for I be non empty set, M be non-empty ManySortedSet of I holds M = [0]I +* (M|supp M); theorem :: CLOSURE3:7 for I be non empty set, M1, M2 be non-empty ManySortedSet of I holds supp M1 = supp M2 & M1|supp M1 = M2|supp M2 implies M1 = M2; theorem :: CLOSURE3:8 for I be non empty set, M be ManySortedSet of I, x be Element of I holds (not x in supp M) implies M.x = {}; theorem :: CLOSURE3:9 for I being non empty set, M being ManySortedSet of I, x being Element of Bool M, i being Element of I for y being set st y in x.i ex a being Element of Bool M st y in a.i & a is locally-finite & supp a is finite & a c= x; definition let I be set, M be ManySortedSet of I; let A be SubsetFamily of M; func MSUnion A -> ManySortedSubset of M means :: CLOSURE3:def 4 for i be set st i in I holds it.i = union { f.i where f is Element of Bool M: f in A }; end; definition let I be set, M be ManySortedSet of I; let B be non empty SubsetFamily of M; redefine mode Element of B -> ManySortedSet of I; end; definition let I be set, M be ManySortedSet of I, A be empty SubsetFamily of M; cluster MSUnion A -> empty-yielding; end; theorem :: CLOSURE3:10 for I be set, M be ManySortedSet of I, A be SubsetFamily of M holds MSUnion A = union |:A:|; definition let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M; redefine func A \/ B -> SubsetFamily of M; end; theorem :: CLOSURE3:11 for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M holds MSUnion (A \/ B) = MSUnion A \/ MSUnion B; theorem :: CLOSURE3:12 for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M holds A c= B implies MSUnion A c= MSUnion B; definition let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M; redefine func A /\ B -> SubsetFamily of M; end; theorem :: CLOSURE3:13 for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M holds MSUnion (A /\ B) c= MSUnion A /\ MSUnion B; theorem :: CLOSURE3:14 for I be set, M be ManySortedSet of I, AA be set st for x being set st x in AA holds x is SubsetFamily of M for A,B be SubsetFamily of M st B = { MSUnion X where X is SubsetFamily of M : X in AA} & A = union AA holds MSUnion B = MSUnion A; begin ::Algebraic Operation on Subsets of Many Sorted Sets definition let I be non empty set, M be ManySortedSet of I, S be SetOp of M; attr S is algebraic means :: CLOSURE3:def 5 for x be Element of Bool M st x = S.x ex A be SubsetFamily of M st A = { S.a where a is Element of Bool M : a is locally-finite & supp a is finite & a c= x} & x = MSUnion A; end; definition let I be non empty set, M be ManySortedSet of I; cluster algebraic reflexive monotonic idempotent SetOp of M; end; definition let S be non empty 1-sorted, IT be ClosureSystem of S; attr IT is algebraic means :: CLOSURE3:def 6 ClSys->ClOp IT is algebraic; end; definition let S be non void non empty ManySortedSign, MA be non-empty MSAlgebra over S; func SubAlgCl MA -> strict ClosureStr over the 1-sorted of S means :: CLOSURE3:def 7 the Sorts of it = the Sorts of MA & the Family of it = SubSort MA; end; canceled; theorem :: CLOSURE3:16 for S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA; definition let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> absolutely-multiplicative; end; definition let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> algebraic; end;

Back to top