:: Algebraic Operation on Subsets of Many Sorted Sets :: by Agnieszka Julia Marasik :: :: Received June 23, 1997 :: Copyright (c) 1997-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, STRUCT_0, PBOOLE, FUNCT_4, RELAT_1, CLOSURE2, SETFAM_1, MSUALG_1, TARSKI, MSUALG_2, UNIALG_2, MSSUBFAM, FUNCT_1, MARGREL1, SUBSET_1, FINSET_1, FUNCOP_1, WAYBEL_8, RELAT_2, MSAFREE2, BINOP_1, ZFMISC_1, CARD_3, FUNCT_2, CLOSURE3, PRE_POLY, SETLIM_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, FINSET_1, FUNCT_4, FUNCOP_1, PBOOLE, FINSEQ_2, MSUALG_1, MSUALG_2, CARD_3, PRE_POLY, CLOSURE2, MSSUBFAM, MBOOLEAN; constructors SETFAM_1, FUNCT_4, MSSUBFAM, MSUALG_2, PRALG_2, CLOSURE2, RELSET_1, FINSEQ_2, PRE_POLY; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, PBOOLE, STRUCT_0, MSUALG_1, CLOSURE2, FINSEQ_1; requirements SUBSET, BOOLE; begin :: Preliminaries registration 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 theorem :: CLOSURE3:4 for A,B,C be set 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; redefine func support M equals :: CLOSURE3:def 1 { x where x is Element of I : M.x <> {} }; end; theorem :: CLOSURE3:5 for I be non empty set, M be non-empty ManySortedSet of I holds M = EmptyMS I +* (M|support M); theorem :: CLOSURE3:6 for I be non empty set, M1, M2 be non-empty ManySortedSet of I holds M1|support M1 = M2|support M2 implies M1 = M2; ::$CT theorem :: CLOSURE3:8 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 finite-yielding & support 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 2 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; registration let I be set, M be ManySortedSet of I, A be empty SubsetFamily of M; cluster MSUnion A -> empty-yielding; end; theorem :: CLOSURE3:9 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:10 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:11 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:12 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:13 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 3 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 finite-yielding & support a is finite & a c= x} & x = MSUnion A; end; registration let I be non empty set, M be ManySortedSet of I; cluster algebraic reflexive monotonic idempotent for SetOp of M; end; definition let S be non empty 1-sorted, IT be ClosureSystem of S; attr IT is algebraic means :: CLOSURE3:def 4 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 5 the Sorts of it = the Sorts of MA & the Family of it = SubSort MA; end; theorem :: CLOSURE3:14 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; registration let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> absolutely-multiplicative; end; registration let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> algebraic; end;