:: Algebraic Operation on Subsets of Many Sorted Sets
:: by Agnieszka Julia Marasik
::
:: Received June 23, 1997
:: Copyright (c) 1997-2017 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;