:: Algebraic Operation on Subsets of Many Sorted Sets
:: by Agnieszka Julia Marasik
::
:: Received June 23, 1997
:: Copyright (c) 1997-2026 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;
definitions TARSKI, XBOOLE_0, MSUALG_2, SETFAM_1, PBOOLE;
equalities PBOOLE, ORDINAL1;
expansions TARSKI, XBOOLE_0, CLOSURE2, MSUALG_2, SETFAM_1, PBOOLE;
theorems FUNCT_4, FUNCT_1, TARSKI, PBOOLE, MSUALG_1, MBOOLEAN, FUNCOP_1,
MSUALG_2, CLOSURE2, ZFMISC_1, RELAT_1, CARD_3, MSSUBFAM, FUNCT_2,
XBOOLE_0, SETFAM_1, PARTFUN1, FINSET_1, PRE_POLY;
schemes CLASSES1;
begin :: Preliminaries
registration
let S be non empty 1-sorted;
cluster the 1-sorted of S -> non empty;
coherence;
end;
theorem Th1:
for I be non empty set, M, N be ManySortedSet of I holds M +* N = N
proof
let I be non empty set, M, N be ManySortedSet of I;
dom M = I by PARTFUN1:def 2
.= dom N by PARTFUN1:def 2;
hence thesis by FUNCT_4:19;
end;
theorem
for I be set, M, N be ManySortedSet of I, F be SubsetFamily of M holds
N in F implies meet |:F:| c=' N by CLOSURE2:21,MSSUBFAM:43;
theorem Th3:
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
proof
let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra
over S;
let F be SubsetFamily of the Sorts of MA such that
A1: F c= SubSort MA;
let B be MSSubset of MA such that
A2: B = meet |:F:|;
per cases;
suppose
A3: F = {};
set Q = the Sorts of MA;
reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA;
set I = the carrier of S;
FF = EmptyMS I by A3;
then
A4: Q = B by A2,MSSUBFAM:41;
reconsider Q as MSSubset of MA by PBOOLE:def 18;
for o be OperSymbol of S holds Q is_closed_on o
proof
let o be OperSymbol of S;
A5: (the ResultSort of S).o = the_result_sort_of o & dom the ResultSort
of S = the carrier' of S by FUNCT_2:def 1,MSUALG_1:def 2;
Result(o,MA) = (Q * the ResultSort of S).o by MSUALG_1:def 5
.= Q.(the_result_sort_of o) by A5,FUNCT_1:13;
then
A6: rng ((Den(o,MA))|((Q#.(the_arity_of o)))) c= Q.(the_result_sort_of
o) by RELAT_1:def 19;
(the Arity of S).o = the_arity_of o & dom the Arity of S = the
carrier' of S by FUNCT_2:def 1,MSUALG_1:def 1;
then
A7: (Q# * (the Arity of S)).o = Q#.(the_arity_of o) by FUNCT_1:13;
(Q * the ResultSort of S).o = Q.(the_result_sort_of o) by A5,FUNCT_1:13;
hence thesis by A7,A6;
end;
hence thesis by A4;
end;
suppose
A8: F <> {};
set SS = S;
let o be OperSymbol of SS;
set i = (the_result_sort_of o);
A9: (the ResultSort of SS).o = the_result_sort_of o by MSUALG_1:def 2;
A10: dom the ResultSort of SS = the carrier' of SS by FUNCT_2:def 1;
(the Arity of SS).o = the_arity_of o & dom the Arity of SS = the
carrier' of SS by FUNCT_2:def 1,MSUALG_1:def 1;
then
A11: (B# * (the Arity of SS)).o = B#.(the_arity_of o) by FUNCT_1:13;
Result(o,MA) = ((the Sorts of MA) * the ResultSort of SS).o by
MSUALG_1:def 5
.= (the Sorts of MA).(the_result_sort_of o) by A9,A10,FUNCT_1:13;
then
A12: rng ((Den(o,MA))|((B#.(the_arity_of o)))) c= (the Sorts of MA).(
the_result_sort_of o) by RELAT_1:def 19;
A13: rng ((Den(o,MA))|((B#.(the_arity_of o)))) c= B.(the_result_sort_of o )
proof
consider Q be Subset-Family of ((the Sorts of MA).i) such that
A14: Q = |:F:|.i and
A15: B.i = Intersect Q by A2,MSSUBFAM:def 1;
let v be object;
assume
A16: v in rng ((Den(o,MA))|((B#.(the_arity_of o))));
then consider p be object such that
A17: p in dom ((Den(o,MA))|(B#.(the_arity_of o))) and
A18: v = ((Den(o,MA))|(B#.(the_arity_of o))).p by FUNCT_1:def 3;
for Y being set st Y in Q holds v in Y
proof
A19: |:F:|.i = { xx.i where xx is Element of Bool the Sorts of MA : xx
in F } by A8,CLOSURE2:14;
let Y be set;
assume Y in Q;
then consider xx be Element of Bool the Sorts of MA such that
A20: Y = xx.i and
A21: xx in F by A14,A19;
reconsider xx as MSSubset of MA;
xx is opers_closed by A1,A21,MSUALG_2:14;
then xx is_closed_on o;
then
A22: rng ((Den(o,MA))|((xx# * the Arity of SS).o)) c= (xx * the
ResultSort of SS).o;
B c= xx by A2,A21,CLOSURE2:21,MSSUBFAM:43;
then
(Den(o,MA))|((B# * the Arity of SS).o) c= (Den(o,MA))|((xx# * the
Arity of SS).o) by MSUALG_2:2,RELAT_1:75;
then
A23: dom ((Den(o,MA))|((B# * the Arity of SS).o)) c= dom ((Den(o,MA))|
((xx# * the Arity of SS).o)) by RELAT_1:11;
A24: v = (Den(o,MA)).p by A17,A18,FUNCT_1:47;
then v = ((Den(o,MA))|((xx# * the Arity of SS).o)).p by A11,A17,A23,
FUNCT_1:47;
then
v in rng ((Den(o,MA))|((xx# * the Arity of SS).o)) by A11,A17,A23,
FUNCT_1:def 3;
then (Den(o,MA)).p in (xx * the ResultSort of SS).o by A22,A24;
then (Den(o,MA)).p in xx.((the ResultSort of SS).o) by A10,FUNCT_1:13;
then (Den(o,MA)).p in xx.i by MSUALG_1:def 2;
hence thesis by A17,A18,A20,FUNCT_1:47;
end;
hence thesis by A12,A16,A15,SETFAM_1:43;
end;
(B * the ResultSort of SS).o = B.(the_result_sort_of o) by A9,A10,
FUNCT_1:13;
hence thesis by A11,A13;
end;
end;
begin :: Relationships between Subsets Families
theorem
for A,B,C be set holds A is_coarser_than B & B is_coarser_than C
implies A is_coarser_than C
proof
let A,B,C be set;
assume that
A1: A is_coarser_than B and
A2: B is_coarser_than C;
let a be set;
assume a in A;
then consider b be set such that
A3: b in B and
A4: b c= a by A1;
consider c be set such that
A5: c in C & c c= b by A2,A3;
take c;
thus thesis by A4,A5;
end;
Lm1: now
let I be non empty set, M be ManySortedSet of I;
set F = { x where x is Element of I : M.x <> {} };
thus support M = F
proof
thus support M c= F
proof
let x be object;
A1: dom M = I by PARTFUN1:def 2;
A2: support M c= dom M by PRE_POLY:37;
assume
A3: x in support M;
then M.x <> {} by PRE_POLY:def 7;
hence thesis by A1,A2,A3;
end;
let x be object;
assume x in F;
then ex i being Element of I st x = i & M.i <> {};
hence thesis by PRE_POLY:def 7;
end;
end;
definition
let I be non empty set, M be ManySortedSet of I;
redefine func support M equals :: redefines support (PRE_POLY, definition)
{ x where x is Element of I : M.x <> {} };
compatibility by Lm1;
end;
theorem
for I be non empty set, M be non-empty ManySortedSet of I holds
M = EmptyMS I +* (M|support M)
proof
let I be non empty set, M be non-empty ManySortedSet of I;
set MM = M|support M;
A1: I c= support M
proof
let v be object;
assume
A2: v in I;
then M.v <> {};
hence thesis by A2;
end;
dom M = I by PARTFUN1:def 2;
then MM = M by A1,RELAT_1:68;
hence thesis by Th1;
end;
theorem
for I be non empty set, M1, M2 be non-empty ManySortedSet of I holds
M1|support M1 = M2|support M2 implies M1 = M2
proof
let I be non empty set, M1, M2 be non-empty ManySortedSet of I;
A1: dom M1 = I by PARTFUN1:def 2;
A2: dom M2 = I by PARTFUN1:def 2;
assume
A3: M1|support M1 = M2|support M2;
for x be object st x in I holds M1.x = M2.x
proof
let x be object;
A4: dom (M2|support M2) = dom M2 /\ support M2 by RELAT_1:61;
assume
A5: x in I;
then M1.x is non empty;
then
A6: x in support M1 by A5;
M2.x is non empty by A5;
then x in support M2 by A5;
then
A7: x in dom (M2|support M2) by A2,A5,A4,XBOOLE_0:def 4;
dom (M1|support M1) = dom M1 /\ support M1 by RELAT_1:61;
then x in dom (M1|support M1) by A1,A5,A6,XBOOLE_0:def 4;
then M1.x = (M2|support M2).x by A3,FUNCT_1:47
.= M2.x by A7,FUNCT_1:47;
hence thesis;
end;
hence thesis;
end;
::$CT
theorem Th7:
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
proof
let I be non empty set, M be ManySortedSet of I, x be Element of Bool M, i
be Element of I;
let y be set such that
A1: y in x.i;
set N = {i} --> {y};
set A = EmptyMS I +* N;
A2: dom N = {i} by FUNCOP_1:13;
then
A3: i in dom N by TARSKI:def 1;
then
A4: N.i = {y} by A2,FUNCOP_1:7;
then
A5: A.i = {y} by A3,FUNCT_4:13;
A6: dom A = dom EmptyMS I \/ dom N by FUNCT_4:def 1
.= I \/ {i} by A2,PARTFUN1:def 2
.= I by ZFMISC_1:40;
then reconsider A as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
for j be object st j in I holds A.j c= M.j
proof
let j be object such that
A7: j in I;
per cases;
suppose
A8: i = j;
reconsider x as ManySortedSubset of M;
let v be object;
assume v in A.j;
then v in {y} by A3,A4,A8,FUNCT_4:13;
then
A9: v in x.j by A1,A8,TARSKI:def 1;
x c= M by PBOOLE:def 18;
then x.j c= M.j by A7;
hence thesis by A9;
end;
suppose
i <> j;
then
A10: not j in {i} by TARSKI:def 1;
j in dom EmptyMS I \/ dom N by A6,A7,FUNCT_4:def 1;
then A.j = (I --> {}).j by A2,A10,FUNCT_4:def 1
.= {} by A7,FUNCOP_1:7;
hence thesis;
end;
end;
then A c= M;
then reconsider AA = A as ManySortedSubset of M by PBOOLE:def 18;
reconsider a = AA as Element of Bool M by CLOSURE2:def 1;
A11: for j be object st j in I holds a.j c= x.j
proof
let j be object such that
A12: j in I;
per cases;
suppose
A13: i = j;
let v be object;
assume
A14: v in a.j;
a.j = {y} by A3,A4,A13,FUNCT_4:13;
hence thesis by A1,A13,A14,TARSKI:def 1;
end;
suppose
j <> i;
then
A15: not j in {i} by TARSKI:def 1;
j in dom EmptyMS I \/ dom N by A6,A12,FUNCT_4:def 1;
then a.j = (I --> {}).j by A2,A15,FUNCT_4:def 1
.= {} by A12,FUNCOP_1:7;
hence thesis;
end;
end;
A16: { b where b is Element of I : a.b <> {}} = {i}
proof
thus { b where b is Element of I : a.b <> {}} c= {i}
proof
let s be object;
assume s in { b where b is Element of I : a.b <> {}};
then
A17: ex b be Element of I st s = b & a.b <> {};
assume
A18: not s in {i};
reconsider s as Element of I by A17;
s in dom a by A6;
then s in dom EmptyMS I \/ dom N by FUNCT_4:def 1;
then a.s = (I --> {}).s by A2,A18,FUNCT_4:def 1
.= {} by FUNCOP_1:7;
hence contradiction by A17;
end;
let s be object;
assume
A19: s in {i};
then
A20: s = i by TARSKI:def 1;
reconsider s as Element of I by A19,TARSKI:def 1;
a.s = {y} by A3,A4,A20,FUNCT_4:13;
hence thesis;
end;
take a;
for j be object st j in I holds a.j is finite
proof
let j be object such that
A21: j in I;
per cases;
suppose
j = i;
hence thesis by A3,A4,FUNCT_4:13;
end;
suppose
j <> i;
then
A22: not j in {i} by TARSKI:def 1;
j in dom EmptyMS I \/ dom N by A6,A21,FUNCT_4:def 1;
then a.j = (I --> {}).j by A2,A22,FUNCT_4:def 1
.= {} by A21,FUNCOP_1:7;
hence thesis;
end;
end;
hence thesis by A5,A16,A11,FINSET_1:def 5,TARSKI:def 1;
end;
definition
let I be set, M be ManySortedSet of I;
let A be SubsetFamily of M;
func MSUnion A -> ManySortedSubset of M means
:Def2:
for i be set st i in I
holds it.i = union { f.i where f is Element of Bool M: f in A };
existence
proof
defpred P[object,object] means
$2 = union { f.$1 where f is Element of Bool M:f in A };
A1: for x be object st x in I ex y be object st P[x,y];
consider IT be Function such that
A2: dom IT = I and
A3: for x be object st x in I holds P[x, IT.x] from CLASSES1:sch 1(A1);
reconsider IT as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
for i be object st i in I holds IT.i c= M.i
proof
let i be object such that
A4: i in I;
for x be object holds x in IT.i implies x in M.i
proof
let x be object;
assume
A5: x in IT.i;
IT.i = union { f.i where f is Element of Bool M: f in A } by A3,A4;
then consider Y be set such that
A6: x in Y and
A7: Y in { f.i where f is Element of Bool M: f in A } by A5,TARSKI:def 4;
consider ff be Element of Bool M such that
A8: ff.i = Y and
ff in A by A7;
reconsider ff as ManySortedSubset of M;
ff c= M by PBOOLE:def 18;
then ff.i c= M.i by A4;
hence thesis by A6,A8;
end;
hence thesis;
end;
then IT c= M;
then reconsider IT as ManySortedSubset of M by PBOOLE:def 18;
take IT;
thus thesis by A3;
end;
uniqueness
proof
let B1,B2 be ManySortedSubset of M;
assume that
A9: for i be set st i in I holds B1.i = union { f.i where f is
Element of Bool M: f in A } and
A10: for i be set st i in I holds B2.i = union { ff.i where ff is
Element of Bool M: ff in A };
for i be object st i in I holds B1.i = B2.i
proof
let i be object;
assume
A11: i in I;
then B1.i = union { f.i where f is Element of Bool M : f in A } by A9
.= B2.i by A10,A11;
hence thesis;
end;
hence thesis;
end;
end;
registration
let I be set, M be ManySortedSet of I, A be empty SubsetFamily of M;
cluster MSUnion A -> empty-yielding;
coherence
proof
let i be object;
set MA = MSUnion A;
assume i in I;
then
A1: MA.i = union {f.i where f is Element of Bool M : f in A} by Def2;
assume MA.i is non empty;
then consider v being object such that
A2: v in MA.i;
consider h be set such that
v in h and
A3: h in {f.i where f is Element of Bool M : f in A} by A1,A2,TARSKI:def 4;
ex g be Element of Bool M st h = g.i & g in A by A3;
hence contradiction;
end;
end;
theorem
for I be set, M be ManySortedSet of I, A be SubsetFamily of M holds
MSUnion A = union |:A:|
proof
let I be set, M be ManySortedSet of I, A be SubsetFamily of M;
set AA = |:A:|;
reconsider UA = union AA as ManySortedSet of I;
per cases;
suppose
A1: A is non empty;
for i be object st i in I holds (MSUnion A).i = UA.i
proof
let i be object;
assume
A2: i in I;
then
AA.i = { g.i where g is Element of Bool M : g in A } & UA.i = union
(AA.i) by A1,CLOSURE2:14,MBOOLEAN:def 2;
hence thesis by A2,Def2;
end;
hence thesis;
end;
suppose
A3: A is empty SubsetFamily of M;
for i be object st i in I holds (MSUnion A).i = UA.i
proof
let i be object;
assume i in I;
AA = EmptyMS I by A3;
then UA = EmptyMS I by MBOOLEAN:21;
then UA.i is empty;
hence thesis by A3;
end;
hence thesis;
end;
end;
definition
let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M;
redefine func A \/ B -> SubsetFamily of M; :: redefines \/ (XBOOLE_0, definition)
correctness by CLOSURE2:3;
end;
theorem
for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M
holds MSUnion (A \/ B) = MSUnion A (\/) MSUnion B
proof
let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M;
reconsider MAB = MSUnion (A \/ B) as ManySortedSubset of M;
reconsider MAB as ManySortedSet of I;
reconsider MA = MSUnion A as ManySortedSubset of M;
reconsider MA as ManySortedSet of I;
reconsider MB = MSUnion B as ManySortedSubset of M;
reconsider MB as ManySortedSet of I;
for i be object st i in I holds MAB.i = (MA (\/) MB).i
proof
let i be object;
assume
A1: i in I;
then
A2: MAB.i = union {f.i where f is Element of Bool M : f in (A \/ B)} by Def2;
A3: (MA (\/) MB).i = MA.i \/ MB.i by A1,PBOOLE:def 4;
A4: for v be object holds v in (MA (\/) MB).i implies v in MAB.i
proof
let v be object;
assume v in (MA (\/) MB).i;
then
A5: v in MA.i or v in MB.i by A3,XBOOLE_0:def 3;
per cases by A1,A5,Def2;
suppose
v in union { f.i where f is Element of Bool M : f in A};
then consider g be set such that
A6: v in g and
A7: g in { f.i where f is Element of Bool M : f in A} by TARSKI:def 4;
consider h be Element of Bool M such that
A8: g = h.i and
A9: h in A by A7;
h in A \/ B by A9,XBOOLE_0:def 3;
then
g in { f.i where f is Element of Bool M : f in (A \/ B)} by A8;
hence thesis by A2,A6,TARSKI:def 4;
end;
suppose
v in union { f.i where f is Element of Bool M : f in B};
then consider g be set such that
A10: v in g and
A11: g in { f.i where f is Element of Bool M : f in B} by TARSKI:def 4;
consider h be Element of Bool M such that
A12: g = h.i and
A13: h in B by A11;
h in A \/ B by A13,XBOOLE_0:def 3;
then
g in { f.i where f is Element of Bool M : f in (A \/ B)} by A12;
hence thesis by A2,A10,TARSKI:def 4;
end;
end;
A14: MA.i = union {f.i where f is Element of Bool M : f in A } & MB.i =
union {f. i where f is Element of Bool M : f in B } by A1,Def2;
for v be object holds v in MAB.i implies v in (MA (\/) MB).i
proof
let v be object;
assume v in MAB.i;
then consider h be set such that
A15: v in h and
A16: h in {f.i where f is Element of Bool M : f in (A \/ B)} by A2,
TARSKI:def 4;
consider g be Element of Bool M such that
A17: h = g.i and
A18: g in (A \/ B) by A16;
g in A or g in B by A18,XBOOLE_0:def 3;
then h in {f.i where f is Element of Bool M : f in A } or h in {f.i
where f is Element of Bool M : f in B } by A17;
then v in union {f.i where f is Element of Bool M : f in A } or v in
union {f.i where f is Element of Bool M : f in B } by A15,TARSKI:def 4;
hence thesis by A3,A14,XBOOLE_0:def 3;
end;
hence thesis by A4,TARSKI:2;
end;
hence thesis;
end;
theorem
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
proof
let I be set, M be ManySortedSet of I;
let A, B be SubsetFamily of M;
reconsider MA = MSUnion A as ManySortedSubset of M;
reconsider MA as ManySortedSet of I;
reconsider MB = MSUnion B as ManySortedSubset of M;
reconsider MB as ManySortedSet of I;
assume
A1: A c= B;
for i be object st i in I holds MA.i c= MB.i
proof
let i be object such that
A2: i in I;
for v be object st v in MA.i holds v in MB.i
proof
A3: MA.i = union {f.i where f is Element of Bool M : f in A} by A2,Def2;
let v be object;
assume v in MA.i;
then consider h be set such that
A4: v in h and
A5: h in {f.i where f is Element of Bool M : f in A} by A3,TARSKI:def 4;
ex g be Element of Bool M st h = g.i & g in A by A5;
then h in {k.i where k is Element of Bool M : k in B} by A1;
then v in union {k.i where k is Element of Bool M : k in B} by A4,
TARSKI:def 4;
hence thesis by A2,Def2;
end;
hence thesis;
end;
hence thesis;
end;
definition
let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M;
redefine func A /\ B -> SubsetFamily of M; :: redefines /\ (XBOOLE_0, definition)
correctness by CLOSURE2:4;
end;
theorem
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
proof
let I be set, M be ManySortedSet of I;
let A, B be SubsetFamily of M;
reconsider MAB = MSUnion (A /\ B) as ManySortedSet of I;
reconsider MA = MSUnion A as ManySortedSet of I;
reconsider MB = MSUnion B as ManySortedSet of I;
for i be object st i in I holds MAB.i c= (MA (/\) MB).i
proof
let i be object;
assume
A1: i in I;
then
A2: MA.i = union {f.i where f is Element of Bool M : f in A } & MB.i =
union {f. i where f is Element of Bool M : f in B } by Def2;
A3: MAB.i = union {f.i where f is Element of Bool M : f in (A /\ B)} by A1,Def2
;
for v be object st v in MAB.i holds v in (MA (/\) MB).i
proof
let v be object;
assume v in MAB.i;
then consider w be set such that
A4: v in w and
A5: w in {f.i where f is Element of Bool M : f in (A /\ B)} by A3,
TARSKI:def 4;
consider g be Element of Bool M such that
A6: w = g.i and
A7: g in A /\ B by A5;
g in B by A7,XBOOLE_0:def 4;
then w in {f.i where f is Element of Bool M : f in B } by A6;
then
A8: v in union {f.i where f is Element of Bool M : f in B } by A4,
TARSKI:def 4;
g in A by A7,XBOOLE_0:def 4;
then w in {f.i where f is Element of Bool M : f in A } by A6;
then v in union {f.i where f is Element of Bool M : f in A } by A4,
TARSKI:def 4;
then v in (MA.i /\ MB.i) by A2,A8,XBOOLE_0:def 4;
hence thesis by A1,PBOOLE:def 5;
end;
hence thesis;
end;
hence thesis;
end;
theorem
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
proof
let I be set, M be ManySortedSet of I, AA be set such that
A1: for x being set st x in AA holds x is SubsetFamily of M;
let A,B be SubsetFamily of M such that
A2: B = { MSUnion X where X is SubsetFamily of M : X in AA} and
A3: A = union AA;
let i be object such that
A4: i in I;
thus (MSUnion B).i c= (MSUnion A).i
proof
let a be object;
thus a in (MSUnion B).i implies a in (MSUnion A).i
proof
assume a in (MSUnion B).i;
then a in union { f.i where f is Element of Bool M: f in B} by A4,Def2;
then consider Y be set such that
A5: a in Y and
A6: Y in { f.i where f is Element of Bool M: f in B} by TARSKI:def 4;
consider f be Element of Bool M such that
A7: f.i = Y and
A8: f in B by A6;
consider Q be SubsetFamily of M such that
A9: f = MSUnion Q and
A10: Q in AA by A2,A8;
(MSUnion Q).i = union { g.i where g is Element of Bool M : g in Q
} by A4,Def2;
then consider d be set such that
A11: a in d and
A12: d in { g.i where g is Element of Bool M : g in Q} by A5,A7,A9,
TARSKI:def 4;
consider g be Element of Bool M such that
A13: d = g.i and
A14: g in Q by A12;
g in union AA by A10,A14,TARSKI:def 4;
then
d in { h.i where h is Element of Bool M: h in union AA } by A13;
then
a in union { h.i where h is Element of Bool M: h in union AA } by A11,
TARSKI:def 4;
hence thesis by A3,A4,Def2;
end;
end;
let a be object;
assume a in (MSUnion A).i;
then a in union { f.i where f is Element of Bool M: f in A} by A4,Def2;
then consider Y be set such that
A15: a in Y and
A16: Y in { f.i where f is Element of Bool M: f in A} by TARSKI:def 4;
consider f be Element of Bool M such that
A17: f.i = Y and
A18: f in A by A16;
consider c be set such that
A19: f in c and
A20: c in AA by A3,A18,TARSKI:def 4;
reconsider c as SubsetFamily of M by A1,A20;
f.i in {v.i where v is Element of Bool M: v in c} by A19;
then
A21: a in union {v.i where v is Element of Bool M: v in c} by A15,A17,
TARSKI:def 4;
(MSUnion c).i = union {v.i where v is Element of Bool M: v in c} by A4
,Def2;
then consider cos be set such that
A22: a in cos and
A23: cos = (MSUnion c).i by A21;
MSUnion c in { MSUnion X where X is SubsetFamily of M : X in AA } by A20;
then cos in { t.i where t is Element of Bool M : t in B} by A2,A23;
then a in union { t.i where t is Element of Bool M : t in B} by A22,
TARSKI:def 4;
hence thesis by A4,Def2;
end;
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
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;
existence
proof
reconsider f = id (Bool M) as SetOp of M;
take f;
thus f is algebraic
proof
let x be Element of Bool M such that
x = f.x;
set A = { f.a where a is Element of Bool M : a is finite-yielding &
support a is finite & a c= x};
A c= Bool M
proof
let v be object;
assume v in A;
then
ex a be Element of Bool M st v = f.a & a is finite-yielding & support
a is finite & a c= x;
hence thesis;
end;
then reconsider A as SubsetFamily of M;
take A;
thus A = { f.a where a is Element of Bool M : a is finite-yielding &
support a is finite & a c= x};
let i be Element of I;
thus x.i c= (MSUnion A).i
proof let y be object;
assume y in x.i;
then consider a be Element of Bool M such that
A1: y in a.i and
A2: a is finite-yielding & support a is finite & a c= x by Th7;
a = f.a;
then a in A by A2;
then a.i in {g.i where g is Element of Bool M : g in A};
then y in union {g.i where g is Element of Bool M : g in A} by A1,
TARSKI:def 4;
hence thesis by Def2;
end;
let v be object;
assume v in (MSUnion A).i;
then
v in union {ff.i where ff is Element of Bool M: ff in A} by Def2;
then consider Y be set such that
A3: v in Y and
A4: Y in {ff.i where ff is Element of Bool M: ff in A} by TARSKI:def 4;
consider ff be Element of Bool M such that
A5: Y = ff.i and
A6: ff in A by A4;
consider a be Element of Bool M such that
A7: ff = f.a and
a is finite-yielding and
support a is finite and
A8: a c= x by A6;
ff = a by A7;
then ff.i c= x.i by A8;
hence thesis by A3,A5;
end;
thus f is reflexive;
thus f is monotonic;
thus f is idempotent;
end;
end;
definition
let S be non empty 1-sorted, IT be ClosureSystem of S;
attr IT is algebraic means
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
:Def5:
the Sorts of it = the Sorts of MA & the Family of it = SubSort MA;
existence
proof
reconsider SS = the Sorts of MA as ManySortedSet of the carrier of the
1-sorted of S;
SubSort MA c= Bool the Sorts of MA
proof
let x be object;
assume x in SubSort MA;
then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;
hence thesis by CLOSURE2:def 1;
end;
then reconsider SF = SubSort MA as SubsetFamily of SS;
take ClosureStr (#SS, SF#);
thus thesis;
end;
uniqueness;
end;
theorem Th13:
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
proof
let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra
over S;
SubSort MA c= Bool the Sorts of MA
proof
let x be object;
assume x in SubSort MA;
then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;
hence thesis by CLOSURE2:def 1;
end;
then reconsider SUBMA = SubSort MA as SubsetFamily of the Sorts of MA;
for F be SubsetFamily of the Sorts of MA st F c= SUBMA holds meet |:F:|
in SUBMA
proof
set M = bool (Union (the Sorts of MA));
set I = the carrier of S;
let F be SubsetFamily of the Sorts of MA such that
A1: F c= SUBMA;
set x = meet |:F:|;
A2: dom x = I by PARTFUN1:def 2;
rng x c= M
proof
let u be object;
reconsider uu=u as set by TARSKI:1;
assume u in rng x;
then consider i be object such that
A3: i in dom x and
A4: u = x.i by FUNCT_1:def 3;
dom (the Sorts of MA) = I by PARTFUN1:def 2;
then (the Sorts of MA).i in rng (the Sorts of MA) by A2,A3,FUNCT_1:def 3;
then
A5: (the Sorts of MA).i c= union rng (the Sorts of MA) by ZFMISC_1:74;
ex Q be Subset-Family of (the Sorts of MA).i st Q = |:F:|. i & u =
Intersect Q by A2,A3,A4,MSSUBFAM:def 1;
then uu c= union rng (the Sorts of MA) by A5;
then u in bool (union rng (the Sorts of MA));
hence thesis by CARD_3:def 4;
end;
then
A6: x in Funcs ( I, M) by A2,FUNCT_2:def 2;
reconsider x as MSSubset of MA;
for B be MSSubset of MA st B = x holds B is opers_closed by A1,Th3;
hence thesis by A6,MSUALG_2:def 11;
end;
hence thesis by CLOSURE2:def 7;
end;
registration
let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra
over S;
cluster SubAlgCl MA -> absolutely-multiplicative;
coherence
proof
thus SubAlgCl MA is absolutely-multiplicative
proof
reconsider SF = SubSort MA as absolutely-multiplicative SubsetFamily of
the Sorts of MA by Th13;
set F = the Family of SubAlgCl MA;
the Sorts of SubAlgCl MA = the Sorts of MA & F = SF by Def5;
hence thesis;
end;
end;
end;
registration
let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra
over S;
cluster SubAlgCl MA -> algebraic;
coherence
proof
set I = the carrier of S;
set SS = ClSys->ClOp SubAlgCl MA, M = the Sorts of SubAlgCl MA;
let x be Element of Bool M such that
A1: x = SS.x;
set A = { SS.a where a is Element of Bool M : a is finite-yielding &
support a is finite & a c= x};
A c= Bool M
proof
let v be object;
assume v in A;
then
ex a be Element of Bool M st v = SS.a & a is finite-yielding & support a
is finite & a c= x;
then reconsider vv = v as Element of Bool M;
vv in Bool M;
hence thesis;
end;
then reconsider A as SubsetFamily of M;
take A;
thus A = { SS.b where b is Element of Bool M : b is finite-yielding &
support b is finite & b c= x};
reconsider y = x, z = MSUnion A as ManySortedSet of I;
y = z
proof
let i be Element of I;
reconsider SS9 = SS as reflexive SetOp of M;
thus y.i c= z.i
proof
let v be object;
assume v in y.i;
then consider b be Element of Bool M such that
A2: v in b.i and
A3: b is finite-yielding & support b is finite & b c= x by Th7;
b c=' SS9.b by CLOSURE2:def 10;
then
A4: b.i c= (SS9.b).i;
SS.b in A by A3;
then (SS9.b).i in {f.i where f is Element of Bool M : f in A};
then v in union {f.i where f is Element of Bool M : f in A} by A2,A4,
TARSKI:def 4;
hence thesis by Def2;
end;
reconsider SS9 = SS as monotonic SetOp of M;
let v be object;
assume v in z.i;
then v in union {ff.i where ff is Element of Bool M: ff in A} by Def2;
then consider Y be set such that
A5: v in Y and
A6: Y in {ff.i where ff is Element of Bool M: ff in A} by TARSKI:def 4;
consider ff be Element of Bool M such that
A7: Y = ff.i and
A8: ff in A by A6;
consider a be Element of Bool M such that
A9: ff = SS.a and
a is finite-yielding and
support a is finite and
A10: a c=' x by A8;
SS9.a c=' SS9.x by A10,CLOSURE2:def 11;
then ff.i c= x.i by A1,A9;
hence thesis by A5,A7;
end;
hence thesis;
end;
end;