:: Certain Facts about Families of Subsets of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received October 27, 1995
:: Copyright (c) 1995-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 PBOOLE, FUNCT_6, RELAT_1, PARTFUN1, FUNCT_1, SETFAM_1, SUBSET_1,
FINSET_1, XBOOLE_0, TARSKI, MEMBER_1, PZFMISC1, ZFMISC_1, FUNCT_4,
FUNCOP_1, FUNCT_2, ORDINAL1, MSSUBFAM, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FUNCT_4, FUNCT_6,
PBOOLE, MBOOLEAN, PZFMISC1;
constructors SETFAM_1, FUNCT_4, FUNCT_6, MBOOLEAN, PZFMISC1, PARTFUN1,
RELSET_1, ORDINAL1, PBOOLE, FINSET_1;
registrations XBOOLE_0, FUNCT_1, FUNCOP_1, FINSET_1, PBOOLE, PRE_CIRC,
MBOOLEAN, PZFMISC1, FUNCT_2, PARTFUN1, CARD_1, RELSET_1, RELAT_1;
requirements SUBSET, BOOLE;
definitions XBOOLE_0, PBOOLE, FINSET_1, ORDINAL1;
equalities PBOOLE, FUNCOP_1;
expansions XBOOLE_0, PBOOLE;
theorems FUNCOP_1, FINSET_1, ORDERS_1, FRAENKEL, FUNCT_2, FUNCT_4, FUNCT_6,
MBOOLEAN, PBOOLE, PZFMISC1, SETFAM_1, TARSKI, RELSET_1, XBOOLE_0,
XBOOLE_1, RELAT_1, PARTFUN1;
schemes FUNCT_2, PBOOLE;
begin :: Preliminaries
registration
let I be set;
let F be ManySortedFunction of I;
cluster doms F -> I-defined;
coherence
proof
dom doms F = dom F by FUNCT_6:59
.= I by PARTFUN1:def 2;
hence thesis by RELAT_1:def 18;
end;
cluster rngs F -> I-defined;
coherence
proof
dom rngs F = dom F by FUNCT_6:60
.= I by PARTFUN1:def 2;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let I be set;
let F be ManySortedFunction of I;
cluster doms F -> total for I-defined Function;
coherence
proof
dom doms F = dom F by FUNCT_6:59
.= I by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
cluster rngs F -> total for I-defined Function;
coherence
proof
dom rngs F = dom F by FUNCT_6:60
.= I by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
end;
reserve I, G, H for set, i, x for object,
A, B, M for ManySortedSet of I,
sf, sg, sh for Subset-Family of I,
v, w for Subset of I,
F for ManySortedFunction of I;
scheme
MSFExFunc { I() -> set, A, B() -> ManySortedSet of I(),
P[object,object,object] } :
ex F be ManySortedFunction of A(), B() st
for i be object st i in I() holds ex f
be Function of A().i, B().i st f = F.i &
for x be object st x in A().i holds P[f.x,x,i]
provided
A1: for i be object st i in I() for x be object st x in A().i
ex y be object st y in B().i & P[y,x,i]
proof
defpred Q[object,object] means
ex f1 be Function of A().$1, B().$1 st f1 = $2 &
for x be object st x in A().$1 holds P[f1.x,x,$1];
A2: now
let i be object such that
A3: i in I();
per cases;
suppose
B().i is non empty;
then reconsider bb = B().i as non empty set;
defpred Z[object,object] means P[ $2,$1,i];
A4: for e be object st e in A().i
ex u be object st u in bb & Z[e,u] by A1,A3;
consider ff be Function of A().i, bb such that
A5: for e be object st e in A().i holds Z[e,ff.e] from FUNCT_2:sch 1(A4
);
reconsider fff = ff as Function of A().i, B().i;
reconsider j = fff as object;
take j;
thus Q[i,j] by A5;
end;
suppose
A6: B().i is empty;
A7: now
let x be object;
for y be object holds not (y in B().i & P[y,x,i]) by A6;
hence not x in A().i by A1,A3;
end;
then A().i = {} by XBOOLE_0:def 1;
then reconsider fff = {} as Function of A().i, B().i by RELSET_1:12;
reconsider j = fff as object;
take j;
thus Q[i,j]
proof
take fff;
thus fff = j;
thus thesis by A7;
end;
end;
end;
consider F be ManySortedSet of I() such that
A8: for i be object st i in I() holds Q[i,F.i] from PBOOLE:sch 3(A2);
F is ManySortedFunction of A(), B()
proof
let i be object;
assume i in I();
then
ex f be Function of A().i, B().i st f = F.i &
for x be object st x in A().i holds P[f.x,x,i] by A8;
hence thesis;
end;
then reconsider F as ManySortedFunction of A(), B();
take F;
thus thesis by A8;
end;
theorem :: SETFAM_1:3
sf <> {} implies Intersect sf c= union sf
proof
assume sf <> {};
then Intersect sf = meet sf by SETFAM_1:def 9;
hence thesis by SETFAM_1:2;
end;
theorem :: SETFAM_1:4
G in sf implies Intersect sf c= G
proof
assume
A1: G in sf;
then meet sf = Intersect sf by SETFAM_1:def 9;
hence thesis by A1,SETFAM_1:3;
end;
theorem :: SETFAM_1:5
{} in sf implies Intersect sf = {}
proof
assume
A1: {} in sf;
then Intersect sf = meet sf by SETFAM_1:def 9;
hence thesis by A1,SETFAM_1:4;
end;
theorem :: SETFAM_1:6
for Z be Subset of I holds (for Z1 be set st Z1 in sf holds Z c= Z1)
implies Z c= Intersect sf
proof
let Z be Subset of I such that
A1: for Z1 be set st Z1 in sf holds Z c= Z1;
per cases;
suppose
A2: sf <> {};
then Intersect sf = meet sf by SETFAM_1:def 9;
hence thesis by A1,A2,SETFAM_1:5;
end;
suppose
sf = {};
then Intersect sf = I by SETFAM_1:def 9;
hence thesis;
end;
end;
theorem :: SETFAM_1:6
sf <> {} & (for Z1 be set st Z1 in sf holds G c= Z1) implies G c=
Intersect sf
proof
assume that
A1: sf <> {} and
A2: for Z1 be set st Z1 in sf holds G c= Z1;
Intersect sf = meet sf by A1,SETFAM_1:def 9;
hence thesis by A1,A2,SETFAM_1:5;
end;
theorem :: SETFAM_1:8
G in sf & G c= H implies Intersect sf c= H
proof
assume that
A1: G in sf and
A2: G c= H;
Intersect sf = meet sf by A1,SETFAM_1:def 9;
hence thesis by A1,A2,SETFAM_1:7;
end;
theorem :: SETFAM_1:9
G in sf & G misses H implies Intersect sf misses H
proof
assume that
A1: G in sf and
A2: G misses H;
Intersect sf = meet sf by A1,SETFAM_1:def 9;
hence thesis by A1,A2,SETFAM_1:8;
end;
theorem :: SETFAM_1:10
sh = sf \/ sg implies Intersect sh = Intersect sf /\ Intersect sg
proof
assume
A1: sh = sf \/ sg;
per cases;
suppose
sf = {} & sg = {};
hence thesis by A1;
end;
suppose
A2: sf <> {} & sg = {};
hence Intersect sh = meet sf by A1,SETFAM_1:def 9
.= meet sf /\ I by XBOOLE_1:28
.= Intersect sf /\ I by A2,SETFAM_1:def 9
.= Intersect sf /\ Intersect sg by A2,SETFAM_1:def 9;
end;
suppose
A3: sf = {} & sg <> {};
hence Intersect sh = meet sg by A1,SETFAM_1:def 9
.= I /\ meet sg by XBOOLE_1:28
.= I /\ Intersect sg by A3,SETFAM_1:def 9
.= Intersect sf /\ Intersect sg by A3,SETFAM_1:def 9;
end;
suppose
A4: sf <> {} & sg <> {};
then
A5: Intersect sg = meet sg by SETFAM_1:def 9;
Intersect sh = meet sh & Intersect sf = meet sf by A1,A4,SETFAM_1:def 9;
hence thesis by A1,A4,A5,SETFAM_1:9;
end;
end;
theorem :: SETFAM_1:11
sf = {v} implies Intersect sf = v
proof
assume
A1: sf = {v};
then Intersect sf = meet sf by SETFAM_1:def 9;
hence thesis by A1,SETFAM_1:10;
end;
theorem :: SETFAM_1:12
sf = { v,w } implies Intersect sf = v /\ w
proof
assume
A1: sf = {v,w};
then Intersect sf = meet sf by SETFAM_1:def 9;
hence thesis by A1,SETFAM_1:11;
end;
theorem
A in B implies A is Element of B
proof
assume
A1: A in B;
let i be object;
assume i in I;
hence thesis by A1;
end;
theorem
for B be non-empty ManySortedSet of I holds A is Element of B implies A in B
proof
let B be non-empty ManySortedSet of I;
assume
A1: A is Element of B;
let i be object;
assume
A2: i in I;
then
A3: B.i <> {};
A.i is Element of B.i by A1,A2,PBOOLE:def 14;
hence thesis by A3;
end;
theorem Th13:
for f be Function st i in I & f = F.i holds (rngs F).i = rng f
proof
A1: dom F = I by PARTFUN1:def 2;
let f be Function;
assume i in I & f = F.i;
hence thesis by A1,FUNCT_6:22;
end;
theorem Th14:
for f be Function st i in I & f = F.i holds (doms F).i = dom f
proof
A1: dom F = I by PARTFUN1:def 2;
let f be Function;
assume i in I & f = F.i;
hence thesis by A1,FUNCT_6:22;
end;
theorem
for F, G be ManySortedFunction of I holds G ** F is ManySortedFunction of I
proof
let F, G be ManySortedFunction of I;
dom (G ** F) = (dom F) /\ (dom G) by PBOOLE:def 19
.= I /\ (dom G) by PARTFUN1:def 2
.= I /\ I by PARTFUN1:def 2
.= I;
hence thesis by PARTFUN1:def 2,RELAT_1:def 18;
end;
theorem
for A be non-empty ManySortedSet of I for F be ManySortedFunction of A
, EmptyMS I holds F = EmptyMS I
proof
let A be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, EmptyMS I;
now
let i be object;
assume i in I;
then reconsider f = F.i as Function of A.i, EmptyMS I.i by PBOOLE:def 15;
f = {};
hence F.i = EmptyMS I.i;
end;
hence thesis;
end;
theorem
A is_transformable_to B & F is ManySortedFunction of A, B implies
doms F = A & rngs F c= B
proof
assume that
A1: A is_transformable_to B and
A2: F is ManySortedFunction of A, B;
now
let i be object;
assume
A3: i in I;
then reconsider f = F.i as Function of A.i, B.i by A2,PBOOLE:def 15;
A4: B.i = {} implies A.i = {} by A1,A3,PZFMISC1:def 3;
thus (doms F).i = dom f by A3,Th14
.= A.i by A4,FUNCT_2:def 1;
end;
hence doms F = A;
let i be object;
assume
A5: i in I;
then reconsider f = F.i as Function of A.i, B.i by A2,PBOOLE:def 15;
rng f c= B.i by RELAT_1:def 19;
hence thesis by A5,Th13;
end;
begin :: Finite Many Sorted Sets
registration
let I;
cluster empty-yielding -> finite-yielding for ManySortedSet of I;
coherence
proof
let A be ManySortedSet of I such that
A1: A is empty-yielding;
let i be object;
assume i in I;
reconsider B = A.i as empty set by A1;
B is finite;
hence thesis;
end;
end;
registration
let I;
cluster EmptyMS I -> empty-yielding finite-yielding;
coherence;
end;
registration
let I, A;
cluster empty-yielding finite-yielding for ManySortedSubset of A;
existence
proof
set x = EmptyMS I;
x c= A by PBOOLE:43;
then reconsider x as ManySortedSubset of A by PBOOLE:def 18;
take x;
thus thesis;
end;
end;
theorem Th18:
A c= B & B is finite-yielding implies A is finite-yielding
proof
assume
A1: A c= B & B is finite-yielding;
let i be object;
assume i in I;
then A.i c= B.i & B.i is finite by A1;
hence thesis;
end;
registration
let I;
let A be finite-yielding ManySortedSet of I;
cluster -> finite-yielding for ManySortedSubset of A;
coherence
by PBOOLE:def 18,Th18;
end;
registration
let I;
let A, B be finite-yielding ManySortedSet of I;
cluster A (\/) B -> finite-yielding;
coherence
proof
let i be object;
assume
A1: i in I;
A.i \/ B.i is finite;
hence thesis by A1,PBOOLE:def 4;
end;
end;
registration
let I, A;
let B be finite-yielding ManySortedSet of I;
cluster A (/\) B -> finite-yielding;
coherence
proof
let i be object;
assume
A1: i in I;
A.i /\ B.i is finite;
hence thesis by A1,PBOOLE:def 5;
end;
end;
registration
let I, B;
let A be finite-yielding ManySortedSet of I;
cluster A (/\) B -> finite-yielding;
coherence;
end;
registration
let I, B;
let A be finite-yielding ManySortedSet of I;
cluster A (\) B -> finite-yielding;
coherence
proof
let i be object;
assume
A1: i in I;
A.i \ B.i is finite;
hence thesis by A1,PBOOLE:def 6;
end;
end;
registration
let I, F;
let A be finite-yielding ManySortedSet of I;
cluster F.:.:A -> finite-yielding;
coherence
proof
let i be object such that
A1: i in I;
reconsider f = F.i as Function;
f.:(A.i) is finite;
hence thesis by A1,PBOOLE:def 20;
end;
end;
registration
let I;
let A, B be finite-yielding ManySortedSet of I;
cluster [|A,B|] -> finite-yielding;
coherence
proof
let i be object;
assume
A1: i in I;
[:A.i,B.i:] is finite;
hence thesis by A1,PBOOLE:def 16;
end;
end;
theorem :: FINSET_1:22
B is non-empty & [|A,B|] is finite-yielding implies A is finite-yielding
proof
assume that
A1: B is non-empty and
A2: [|A,B|] is finite-yielding;
let i be object;
assume
A3: i in I;
[|A,B|].i is finite by A2;
then [:A.i,B.i:] is finite by A3,PBOOLE:def 16;
hence thesis by A1,A3;
end;
theorem :: FINSET_1:23
A is non-empty & [|A,B|] is finite-yielding implies B is finite-yielding
proof
assume that
A1: A is non-empty and
A2: [|A,B|] is finite-yielding;
let i be object;
assume
A3: i in I;
[|A,B|].i is finite by A2;
then [:A.i,B.i:] is finite by A3,PBOOLE:def 16;
hence thesis by A1,A3;
end;
theorem Th21:
A is finite-yielding iff bool A is finite-yielding
proof
thus A is finite-yielding implies bool A is finite-yielding
proof
assume
A1: A is finite-yielding;
let i be object;
assume
A2: i in I;
A.i is finite by A1;
then bool (A.i) is finite;
hence thesis by A2,MBOOLEAN:def 1;
end;
assume
A3: bool A is finite-yielding;
let i be object;
assume
A4: i in I;
(bool A).i is finite by A3;
then bool (A.i) is finite by A4,MBOOLEAN:def 1;
hence thesis;
end;
registration
let I;
let M be finite-yielding ManySortedSet of I;
cluster bool M -> finite-yielding;
coherence by Th21;
end;
theorem
for A be non-empty ManySortedSet of I holds A is finite-yielding & (
for M be ManySortedSet of I st M in A holds M is finite-yielding) implies union
A is finite-yielding
proof
let A be non-empty ManySortedSet of I;
assume that
A1: A is finite-yielding and
A2: for M be ManySortedSet of I st M in A holds M is finite-yielding;
let i be object;
assume
A3: i in I;
A4: for X9 be set st X9 in A.i holds X9 is finite
proof
consider M be ManySortedSet of I such that
A5: M in A by PBOOLE:134;
let X9 be set such that
A6: X9 in A.i;
dom (M +* (i .--> X9)) = I by A3,PZFMISC1:1;
then reconsider K = M +* (i .--> X9) as ManySortedSet of I by
PARTFUN1:def 2,RELAT_1:def 18;
A7: dom (i .--> X9) = {i};
i in {i} by TARSKI:def 1;
then
A8: K.i = (i .--> X9).i by A7,FUNCT_4:13
.= X9 by FUNCOP_1:72;
K in A
proof
let j be object such that
A9: j in I;
now
per cases;
case
j = i;
hence thesis by A6,A8;
end;
case
j <> i;
then not j in dom (i .--> X9) by TARSKI:def 1;
then K.j = M.j by FUNCT_4:11;
hence thesis by A5,A9;
end;
end;
hence thesis;
end;
then K is finite-yielding by A2;
hence thesis by A8;
end;
A.i is finite by A1;
then union (A.i) is finite by A4,FINSET_1:7;
hence thesis by A3,MBOOLEAN:def 2;
end;
theorem
union A is finite-yielding implies A is finite-yielding & for M st M
in A holds M is finite-yielding
proof
assume
A1: union A is finite-yielding;
thus A is finite-yielding
proof
let i be object;
assume
A2: i in I;
(union A).i is finite by A1;
then union (A.i) is finite by A2,MBOOLEAN:def 2;
hence thesis by FINSET_1:7;
end;
let M such that
A3: M in A;
let i be object;
assume
A4: i in I;
(union A).i is finite by A1;
then
A5: union (A.i) is finite by A4,MBOOLEAN:def 2;
M.i in A.i by A3,A4;
hence thesis by A5,FINSET_1:7;
end;
theorem :: FINSET_1:26
doms F is finite-yielding implies rngs F is finite-yielding
proof
assume
A1: doms F is finite-yielding;
let i be object such that
A2: i in I;
reconsider f = F.i as Function;
(doms F).i is finite by A1;
then dom f is finite by A2,Th14;
then rng f is finite by FINSET_1:8;
hence thesis by A2,Th13;
end;
theorem :: FINSET_1:27
(A c= rngs F & for i be set for f be Function st i in I & f = F.i
holds f"(A.i) is finite) implies A is finite-yielding
proof
assume that
A1: A c= rngs F and
A2: for i be set for f be Function st i in I & f = F.i holds f"(A.i) is finite;
let i such that
A3: i in I;
reconsider f = F.i as Function;
(rngs F).i = rng f by A3,Th13;
then
A4: A.i c= rng f by A1,A3;
f"(A.i) is finite by A2,A3;
hence thesis by A4,FINSET_1:9;
end;
registration
let I;
let A, B be finite-yielding ManySortedSet of I;
cluster (Funcs)(A,B) -> finite-yielding;
coherence
proof
let i be object;
assume i in I;
then (Funcs)(A,B).i = Funcs(A.i,B.i) & A.i is finite by PBOOLE:def 17;
hence thesis by FRAENKEL:6;
end;
end;
registration
let I;
let A, B be finite-yielding ManySortedSet of I;
cluster A (\+\) B -> finite-yielding;
coherence;
end;
reserve X, Y, Z for ManySortedSet of I;
theorem :: CQC_THE1:13
X is finite-yielding & X c= [|Y,Z|] implies ex A, B st A is
finite-yielding & A c= Y & B is finite-yielding & B c= Z & X c= [|A,B|]
proof
assume that
A1: X is finite-yielding and
A2: X c= [|Y,Z|];
defpred Q[object,object] means
ex D,b be set st D = $2 & D is finite & D c= Y.$1 & b is
finite & b c= Z.$1 & X.$1 c= [:D,b:];
A3: for i being object st i in I ex j be object st Q[i,j]
proof
let i be object;
assume
A4: i in I;
then X.i c= [|Y,Z|].i by A2;
then
A5: X.i c= [:Y.i,Z.i:] by A4,PBOOLE:def 16;
X.i is finite by A1;
then consider A,B being set such that
A6: A is finite & A c= Y.i & B is finite & B c= Z.i &
X.i c= [:A,B:] by A5,FINSET_1:13;
thus thesis by A6;
end;
consider A be ManySortedSet of I such that
A7: for i being object st i in I holds Q[i,A.i] from PBOOLE:sch 3(A3);
defpred P[object,object] means
ex D being set st D = $2 &
A.$1 is finite & A.$1 c= Y.$1 & D is finite & D
c= Z.$1 & X.$1 c= [:A.$1,D:];
A8: for i being object st i in I ex j be object st P[i,j]
proof let i be object;
assume i in I;
then Q[i,A.i] by A7;
hence thesis;
end;
consider B be ManySortedSet of I such that
A9: for i being object st i in I holds P[i,B.i] from PBOOLE:sch 3(A8);
take A, B;
thus A is finite-yielding
proof
let i be object;
assume i in I;
then P[i,B.i] by A9;
hence thesis;
end;
thus A c= Y
proof
let i be object;
assume i in I;
then P[i,B.i] by A9;
hence thesis;
end;
thus B is finite-yielding
proof
let i be object;
assume i in I;
then P[i,B.i] by A9;
hence thesis;
end;
thus B c= Z
proof
let i be object;
assume i in I;
then P[i,B.i] by A9;
hence thesis;
end;
thus X c= [|A,B|]
proof
let i be object;
assume
A10: i in I;
then P[i,B.i] by A9;
then X.i c= [:A.i,B.i:];
hence thesis by A10,PBOOLE:def 16;
end;
end;
theorem :: CQC_THE1:14
X is finite-yielding & X c= [|Y,Z|] implies ex A st A is
finite-yielding & A c= Y & X c= [|A,Z|]
proof
assume that
A1: X is finite-yielding and
A2: X c= [|Y,Z|];
defpred P[object,object] means
ex D being set st D = $2 & D is finite & D c= Y.$1 & X.$1 c= [:D,Z.$1:];
A3: for i being object st i in I ex j be object st P[i,j]
proof
let i be object;
assume
A4: i in I;
then X.i c= [|Y,Z|].i by A2;
then
A5: X.i c= [:Y.i, Z.i:] by A4,PBOOLE:def 16;
X.i is finite by A1;
then consider A9 be set such that
A6: A9 is finite & A9 c= Y.i & X.i c= [:A9,Z.i:] by A5,FINSET_1:14;
take A9;
thus thesis by A6;
end;
consider A such that
A7: for i being object st i in I holds P[i,A.i] from PBOOLE:sch 3(A3);
take A;
thus A is finite-yielding
proof
let i be object;
assume i in I;
then P[i,A.i] by A7;
hence thesis;
end;
thus A c= Y
proof
let i be object;
assume i in I;
then P[i,A.i] by A7;
hence thesis;
end;
thus X c= [|A,Z|]
proof
let i be object;
assume
A8: i in I;
then P[i,A.i] by A7;
then X.i c= [:A.i,Z.i:];
hence thesis by A8,PBOOLE:def 16;
end;
end;
theorem
for M be non-empty finite-yielding ManySortedSet of I st for A, B be
ManySortedSet of I st A in M & B in M holds A c= B or B c= A ex m be
ManySortedSet of I st m in M & for K be ManySortedSet of I st K in M holds m c=
K
proof
let M be non-empty finite-yielding ManySortedSet of I such that
A1: for A, B be ManySortedSet of I st A in M & B in M holds A c= B or B c= A;
defpred Q[object,object] means
ex D being set st D = $2 &
$2 in M.$1 & for D9 be set st D9 in M.$1 holds D c= D9;
A2: for i being object st i in I ex j be object st Q[i,j]
proof
let i be object;
assume
A3: i in I;
M.i is c=-linear
proof
consider c9 be ManySortedSet of I such that
A4: c9 in M by PBOOLE:134;
consider b9 be ManySortedSet of I such that
A5: b9 in M by PBOOLE:134;
let B9, C9 be set such that
A6: B9 in M.i and
A7: C9 in M.i;
A8: dom (i .--> B9) = {i};
set qc = c9 +* (i.-->C9);
dom qc = I by A3,PZFMISC1:1;
then reconsider qc as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18
;
A9: dom (i .--> C9) = {i};
i in {i} by TARSKI:def 1;
then
A10: qc.i = (i .--> C9).i by A9,FUNCT_4:13
.= C9 by FUNCOP_1:72;
A11: qc in M
proof
let j be object such that
A12: j in I;
now
per cases;
case
j = i;
hence thesis by A7,A10;
end;
case
j <> i;
then not j in dom (i .--> C9) by TARSKI:def 1;
then qc.j = c9.j by FUNCT_4:11;
hence thesis by A4,A12;
end;
end;
hence thesis;
end;
set qb = b9 +* (i.-->B9);
dom qb = I by A3,PZFMISC1:1;
then reconsider qb as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18
;
assume
A13: not B9 c= C9;
i in {i} by TARSKI:def 1;
then
A14: qb.i = (i .--> B9).i by A8,FUNCT_4:13
.= B9 by FUNCOP_1:72;
qb in M
proof
let j be object such that
A15: j in I;
now
per cases;
case
j = i;
hence thesis by A6,A14;
end;
case
j <> i;
then not j in dom (i .--> B9) by TARSKI:def 1;
then qb.j = b9.j by FUNCT_4:11;
hence thesis by A5,A15;
end;
end;
hence thesis;
end;
then qb c= qc or qc c= qb by A1,A11;
hence thesis by A3,A13,A14,A10;
end;
then consider m9 be set such that
A16: m9 in M.i & for D9 be set st D9 in M.i holds m9 c= D9 by A3,FINSET_1:11;
take m9;
thus thesis by A16;
end;
consider m be ManySortedSet of I such that
A17: for i being object st i in I holds Q[i,m.i] from PBOOLE:sch 3(A2);
take m;
thus m in M
proof
let i be object;
assume i in I;
then Q[i,m.i] by A17;
hence thesis;
end;
thus for C be ManySortedSet of I st C in M holds m c= C
proof
let C be ManySortedSet of I such that
A18: C in M;
let i be object;
assume
A19: i in I;
then
A20: C.i in M.i by A18;
Q[i,m.i] by A17,A19;
hence thesis by A20;
end;
end;
theorem :: FIN_TOPO:3
for M be non-empty finite-yielding ManySortedSet of I st for A, B be
ManySortedSet of I st A in M & B in M holds A c= B or B c= A ex m be
ManySortedSet of I st m in M & for K be ManySortedSet of I st K in M holds K c=
m
proof
let M be non-empty finite-yielding ManySortedSet of I such that
A1: for A, B be ManySortedSet of I st A in M & B in M holds A c= B or B c= A;
defpred Z[object,object] means
ex X being set st X = $2 &
$2 in M.$1 & for D9 be set st D9 in M.$1 holds D9 c= X;
A2: for i being object st i in I ex j be object st Z[i,j]
proof
let i be object;
assume
A3: i in I;
M.i is c=-linear
proof
consider c9 be ManySortedSet of I such that
A4: c9 in M by PBOOLE:134;
consider b9 be ManySortedSet of I such that
A5: b9 in M by PBOOLE:134;
let B9, C9 be set such that
A6: B9 in M.i and
A7: C9 in M.i;
A8: dom (i .--> B9) = {i};
set qc = c9 +* (i.-->C9);
dom qc = I by A3,PZFMISC1:1;
then reconsider qc as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18
;
A9: dom (i .--> C9) = {i};
i in {i} by TARSKI:def 1;
then
A10: qc.i = (i .--> C9).i by A9,FUNCT_4:13
.= C9 by FUNCOP_1:72;
A11: qc in M
proof
let j be object such that
A12: j in I;
now
per cases;
case
j = i;
hence thesis by A7,A10;
end;
case
j <> i;
then not j in dom (i .--> C9) by TARSKI:def 1;
then qc.j = c9.j by FUNCT_4:11;
hence thesis by A4,A12;
end;
end;
hence thesis;
end;
set qb = b9 +* (i.-->B9);
dom qb = I by A3,PZFMISC1:1;
then reconsider qb as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18
;
assume
A13: not B9 c= C9;
i in {i} by TARSKI:def 1;
then
A14: qb.i = (i .--> B9).i by A8,FUNCT_4:13
.= B9 by FUNCOP_1:72;
qb in M
proof
let j be object such that
A15: j in I;
now
per cases;
case
j = i;
hence thesis by A6,A14;
end;
case
j <> i;
then not j in dom (i .--> B9) by TARSKI:def 1;
then qb.j = b9.j by FUNCT_4:11;
hence thesis by A5,A15;
end;
end;
hence thesis;
end;
then qb c= qc or qc c= qb by A1,A11;
hence thesis by A3,A13,A14,A10;
end;
then consider m9 be set such that
A16: m9 in M.i & for D9 be set st D9 in M.i holds D9 c= m9 by A3,FINSET_1:12;
take m9;
thus thesis by A16;
end;
consider m be ManySortedSet of I such that
A17: for i being object st i in I holds Z[i,m.i] from PBOOLE:sch 3(A2);
take m;
thus m in M
proof
let i be object;
assume i in I;
then Z[i,m.i] by A17;
hence thesis;
end;
thus for K be ManySortedSet of I st K in M holds K c= m
proof
let K be ManySortedSet of I such that
A18: K in M;
let i be object;
assume
A19: i in I;
then
A20: K.i in M.i by A18;
Z[i,m.i] by A17,A19;
hence thesis by A20;
end;
end;
theorem :: COMPTS_1:1
Z is finite-yielding & Z c= rngs F implies ex Y st Y c= doms F & Y is
finite-yielding & F.:.:Y = Z
proof
assume that
A1: Z is finite-yielding and
A2: Z c= rngs F;
defpred P[object,object] means
ex A being set, f be Function st A = $2 & f = F.$1 & A c= (doms F).$1 &
A is finite & f.:A = Z.$1;
A3: for i being object st i in I ex j be object st P[i,j]
proof
let i be object;
reconsider f = F.i as Function;
assume
A4: i in I;
then rng f = (rngs F).i by Th13;
then
A5: Z.i c= rng f by A2,A4;
Z.i is finite by A1;
then consider y be set such that
A6: y c= dom f & y is finite & f.:y = Z.i by A5,ORDERS_1:85;
take y, y, f;
thus y = y;
thus f = F.i;
thus thesis by A4,A6,Th14;
end;
consider Y be ManySortedSet of I such that
A7: for i being object st i in I holds P[i,Y.i] from PBOOLE:sch 3(A3);
take Y;
thus Y c= doms F
proof
let i be object;
assume i in I;
then P[i,Y.i] by A7;
hence thesis;
end;
thus Y is finite-yielding
proof
let i be object;
assume i in I;
then P[i,Y.i] by A7;
hence thesis;
end;
now
let i be object;
assume
A8: i in I;
then P[i,Y.i] by A7;
hence (F.:.:Y).i = Z.i by A8,PBOOLE:def 20;
end;
hence thesis;
end;
begin :: A Family of Subsets of Many Sorted Sets
definition
let I, M;
mode MSSubsetFamily of M is ManySortedSubset of bool M;
end;
registration
let I, M;
cluster non-empty for MSSubsetFamily of M;
existence
proof
bool M is ManySortedSubset of bool M by PBOOLE:def 18;
hence thesis;
end;
end;
definition
let I, M;
redefine func bool M -> MSSubsetFamily of M; :: redefines bool (MBOOLEAN, definition)
coherence by PBOOLE:def 18;
end;
registration
let I, M;
cluster empty-yielding finite-yielding for MSSubsetFamily of M;
existence
proof
EmptyMS I c= bool M by PBOOLE:43;
then EmptyMS I is ManySortedSubset of bool M by PBOOLE:def 18;
hence thesis;
end;
end;
theorem
EmptyMS I is empty-yielding finite-yielding MSSubsetFamily of M
by PBOOLE:43,PBOOLE:def 18;
registration
let I;
let M be finite-yielding ManySortedSet of I;
cluster non-empty finite-yielding for MSSubsetFamily of M;
existence
proof
bool M is MSSubsetFamily of M;
hence thesis;
end;
end;
reserve SF, SG, SH for MSSubsetFamily of M,
SFe for non-empty MSSubsetFamily of M,
V, W for ManySortedSubset of M;
definition
let I be non empty set, M be ManySortedSet of I, SF be MSSubsetFamily of M,
i be Element of I;
redefine func SF.i -> Subset-Family of (M.i); :: redefines . (FUNCT_1, definition)
coherence
proof
SF c= bool M by PBOOLE:def 18;
then SF.i c= (bool M).i;
hence thesis by MBOOLEAN:def 1;
end;
end;
theorem Th32:
i in I implies SF.i is Subset-Family of (M.i)
proof
assume
A1: i in I;
SF c= bool M by PBOOLE:def 18;
then SF.i c= (bool M).i by A1;
hence thesis by A1,MBOOLEAN:def 1;
end;
theorem Th33:
A in SF implies A is ManySortedSubset of M
proof
A1: SF c= bool M by PBOOLE:def 18;
assume A in SF;
then A in bool M by A1,PBOOLE:9;
then A c= M by MBOOLEAN:18;
hence thesis by PBOOLE:def 18;
end;
theorem Th34:
SF (\/) SG is MSSubsetFamily of M
proof
SF c= bool M & SG c= bool M by PBOOLE:def 18;
then SF (\/) SG c= bool M by PBOOLE:16;
hence thesis by PBOOLE:def 18;
end;
theorem
SF (/\) SG is MSSubsetFamily of M
proof
SF c= bool M & SG c= bool M by PBOOLE:def 18;
then SF (/\) SG c= (bool M) (/\) (bool M) by PBOOLE:21;
hence thesis by PBOOLE:def 18;
end;
theorem Th36:
SF (\) A is MSSubsetFamily of M
proof
SF c= bool M by PBOOLE:def 18;
then
A1: SF (\) A c= (bool M) (\) A by PBOOLE:53;
(bool M) (\) A c= bool M by PBOOLE:56;
then SF (\) A c= bool M by A1,PBOOLE:13;
hence thesis by PBOOLE:def 18;
end;
theorem
SF (\+\) SG is MSSubsetFamily of M
proof
SF (\) SG is MSSubsetFamily of M & SG (\) SF is MSSubsetFamily of M by Th36;
hence thesis by Th34;
end;
theorem Th38:
A c= M implies {A} is MSSubsetFamily of M
proof
assume A c= M;
then A in bool M by MBOOLEAN:18;
then {A} c= bool M by PZFMISC1:33;
hence thesis by PBOOLE:def 18;
end;
theorem Th39:
A c= M & B c= M implies {A,B} is MSSubsetFamily of M
proof
assume A c= M & B c= M;
then {A} is MSSubsetFamily of M & {B} is MSSubsetFamily of M by Th38;
then {A} (\/) {B} is MSSubsetFamily of M by Th34;
hence thesis by PZFMISC1:10;
end;
theorem Th40:
union SF c= M
proof
A1: for x being set
for F be Subset-Family of x holds union F is Subset of x;
let i such that
A2: i in I;
SF.i is Subset-Family of M.i by A2,Th32;
then union (SF.i) is Subset of M.i by A1;
then union (SF.i) c= M.i;
hence thesis by A2,MBOOLEAN:def 2;
end;
begin :: Intersection of a Family of Many Sorted Sets
definition
let I, M, SF;
func meet SF -> ManySortedSet of I means
:Def1:
for i be object st i in I holds
ex Q be Subset-Family of (M.i) st Q = SF.i & it.i = Intersect Q;
existence
proof
defpred Z[object,object] means
ex Q be Subset-Family of (M.$1) st Q = SF.$1 & $2
= Intersect Q;
A1: for i being object st i in I ex j be object st Z[i,j]
proof
let i be object;
assume
A2: i in I;
then reconsider Q = SF.i as Subset-Family of (M.i) by Th32;
reconsider a = I --> Intersect Q as ManySortedSet of I;
take a.i;
take Q;
thus thesis by A2,FUNCOP_1:7;
end;
ex X be ManySortedSet of I st for i be object st i in I holds Z[i,X.i]
from PBOOLE:sch 3(A1 );
hence thesis;
end;
uniqueness
proof
let X1, X2 be ManySortedSet of I such that
A3: ( for i being object st i in I
ex Q1 be Subset-Family of M.i st Q1 = SF.i & X1.i = Intersect Q1)
& for i being object st i in I ex Q2 be Subset-Family of M.i
st Q2 = SF.i & X2.i = Intersect Q2;
now
let i be object;
assume i in I;
then
(ex Q1 be Subset-Family of (M.i) st Q1 = SF.i & X1.i = Intersect Q1
)& ex Q2 be Subset-Family of (M.i) st Q2 = SF.i & X2.i = Intersect Q2 by A3;
hence X1.i = X2.i;
end;
hence X1 = X2;
end;
end;
definition
let I, M, SF;
redefine func meet SF -> ManySortedSubset of M; :: redefines meet (MSSUBFAM, definition)
coherence
proof
let i be object;
assume i in I;
then
ex Q be Subset-Family of (M.i) st Q = SF.i & (meet SF).i = Intersect Q
by Def1;
hence thesis;
end;
end;
theorem Th41:
SF = EmptyMS I implies meet SF = M
proof
assume
A1: SF = EmptyMS I;
now
let i be object;
assume i in I;
then consider Q be Subset-Family of (M.i) such that
A2: Q = SF.i and
A3: (meet SF).i = Intersect Q by Def1;
Q = {} by A1,A2;
hence (meet SF).i = M.i by A3,SETFAM_1:def 9;
end;
hence thesis;
end;
theorem :: SETFAM_1:3
meet SFe c= union SFe
proof
let i be object;
assume
A1: i in I;
then consider Q be Subset-Family of (M.i) such that
A2: Q = SFe.i and
A3: (meet SFe).i = Intersect Q by Def1;
meet Q c= union Q & Intersect Q = meet Q by A1,A2,SETFAM_1:2,def 9;
hence thesis by A1,A2,A3,MBOOLEAN:def 2;
end;
theorem :: SETFAM_1:4
A in SF implies meet SF c= A
proof
assume
A1: A in SF;
let i be object;
assume
A2: i in I;
then consider Q be Subset-Family of (M.i) such that
A3: Q = SF.i and
A4: (meet SF).i = Intersect Q by Def1;
A5: A.i in SF.i by A1,A2;
then Intersect Q = meet Q by A3,SETFAM_1:def 9;
hence thesis by A3,A4,A5,SETFAM_1:3;
end;
theorem :: SETFAM_1:5
EmptyMS I in SF implies meet SF = EmptyMS I
proof
assume
A1: EmptyMS I in SF;
now
let i be object;
assume
A2: i in I;
then consider Q be Subset-Family of (M.i) such that
A3: Q = SF.i and
A4: (meet SF).i = Intersect Q by Def1;
EmptyMS I.i in Q by A1,A2,A3;
then
A5: {} in Q;
EmptyMS I.i in SF.i by A1,A2;
then Intersect Q = meet Q by A3,SETFAM_1:def 9;
then Intersect Q = {} by A5,SETFAM_1:4;
hence (meet SF).i = EmptyMS I.i by A4;
end;
hence thesis;
end;
theorem :: SETFAM_1:6
for Z, M be ManySortedSet of I for SF be non-empty MSSubsetFamily of M
st (for Z1 be ManySortedSet of I st Z1 in SF holds Z c= Z1) holds Z c= meet SF
proof
let Z, M be ManySortedSet of I, SF be non-empty MSSubsetFamily of M such
that
A1: for Z1 be ManySortedSet of I st Z1 in SF holds Z c= Z1;
let i be object;
consider T be ManySortedSet of I such that
A2: T in SF by PBOOLE:134;
assume
A3: i in I;
then consider Q be Subset-Family of (M.i) such that
A4: Q = SF.i and
A5: (meet SF).i = Intersect Q by Def1;
A6: for Z9 be set st Z9 in Q holds Z.i c= Z9
proof
let Z9 be set such that
A7: Z9 in Q;
dom (T +* (i .--> Z9)) = I by A3,PZFMISC1:1;
then reconsider K = T +* (i .--> Z9) as ManySortedSet of I by
PARTFUN1:def 2,RELAT_1:def 18;
A8: dom (i .--> Z9) = {i};
i in {i} by TARSKI:def 1;
then
A9: K.i = (i .--> Z9).i by A8,FUNCT_4:13
.= Z9 by FUNCOP_1:72;
K in SF
proof
let q be object such that
A10: q in I;
per cases;
suppose
q = i;
hence thesis by A4,A7,A9;
end;
suppose
q <> i;
then not q in dom (i .--> Z9) by TARSKI:def 1;
then K.q = T.q by FUNCT_4:11;
hence thesis by A2,A10;
end;
end;
then Z c= K by A1;
hence thesis by A3,A9;
end;
Intersect Q = meet Q by A3,A4,SETFAM_1:def 9;
hence thesis by A3,A4,A5,A6,SETFAM_1:5;
end;
theorem :: SETFAM_1:7 :: SETFAM_1:59
SF c= SG implies meet SG c= meet SF
proof
assume
A1: SF c= SG;
let i be object;
assume
A2: i in I;
then consider Qf be Subset-Family of (M.i) such that
A3: Qf = SF.i and
A4: (meet SF).i = Intersect Qf by Def1;
consider Qg be Subset-Family of (M.i) such that
A5: Qg = SG.i and
A6: (meet SG).i = Intersect Qg by A2,Def1;
Qf c= Qg by A1,A2,A3,A5;
hence thesis by A4,A6,SETFAM_1:44;
end;
theorem :: SETFAM_1:8
A in SF & A c= B implies meet SF c= B
proof
assume that
A1: A in SF and
A2: A c= B;
let i be object;
assume
A3: i in I;
then
A4: A.i c= B.i by A2;
consider Q be Subset-Family of (M.i) such that
A5: Q = SF.i and
A6: (meet SF).i = Intersect Q by A3,Def1;
A7: A.i in SF.i by A1,A3;
then Intersect Q = meet Q by A5,SETFAM_1:def 9;
hence thesis by A5,A6,A7,A4,SETFAM_1:7;
end;
theorem :: SETFAM_1:9
A in SF & A (/\) B = EmptyMS I implies meet SF (/\) B = EmptyMS I
proof
assume that
A1: A in SF and
A2: A (/\) B = EmptyMS I;
now
let i be object;
assume
A3: i in I;
then consider Q be Subset-Family of (M.i) such that
A4: Q = SF.i and
A5: (meet SF).i = Intersect Q by Def1;
A6: A.i in SF.i by A1,A3;
A.i /\ B.i = EmptyMS I.i by A2,A3,PBOOLE:def 5;
then A.i /\ B.i = {};
then A.i misses B.i;
then meet Q misses B.i by A4,A6,SETFAM_1:8;
then meet Q /\ B.i = {};
then
A7: meet Q /\ B.i = EmptyMS I.i;
Intersect Q = meet Q by A4,A6,SETFAM_1:def 9;
hence (meet SF (/\) B).i = EmptyMS I.i by A3,A5,A7,PBOOLE:def 5;
end;
hence thesis;
end;
theorem :: SETFAM_1:10
SH = SF (\/) SG implies meet SH = meet SF (/\) meet SG
proof
assume
A1: SH = SF (\/) SG;
now
let i be object;
assume
A2: i in I;
then consider Qf be Subset-Family of (M.i) such that
A3: Qf = SF.i and
A4: (meet SF).i = Intersect Qf by Def1;
consider Qh be Subset-Family of (M.i) such that
A5: Qh = SH.i and
A6: (meet SH).i = Intersect Qh by A2,Def1;
consider Qg be Subset-Family of (M.i) such that
A7: Qg = SG.i and
A8: (meet SG).i = Intersect Qg by A2,Def1;
A9: Qh = Qf \/ Qg by A1,A2,A3,A7,A5,PBOOLE:def 4;
now
per cases;
case
A10: Qf <> {} & Qg <> {};
hence (meet SH).i = meet Qh by A6,A9,SETFAM_1:def 9
.= meet Qf /\ meet Qg by A9,A10,SETFAM_1:9
.= (meet SF).i /\ meet Qg by A4,A10,SETFAM_1:def 9
.= (meet SF).i /\ (meet SG).i by A8,A10,SETFAM_1:def 9
.= (meet SF (/\) meet SG).i by A2,PBOOLE:def 5;
end;
case
A11: Qf <> {} & Qg = {};
hence (meet SH).i = (meet SF).i /\ M.i by A4,A6,A9,XBOOLE_1:28
.= (meet SF).i /\ (meet SG).i by A8,A11,SETFAM_1:def 9
.= (meet SF (/\) meet SG).i by A2,PBOOLE:def 5;
end;
case
A12: Qf = {} & Qg <> {};
hence (meet SH).i = M.i /\ (meet SG).i by A8,A6,A9,XBOOLE_1:28
.= (meet SF).i /\ (meet SG).i by A4,A12,SETFAM_1:def 9
.= (meet SF (/\) meet SG).i by A2,PBOOLE:def 5;
end;
case
Qf = {} & Qg = {};
hence (meet SH).i = Intersect Qf /\ Intersect Qg by A6,A9
.= (meet SF (/\) meet SG).i by A2,A4,A8,PBOOLE:def 5;
end;
end;
hence (meet SH).i = (meet SF (/\) meet SG).i;
end;
hence thesis;
end;
theorem :: SETFAM_1:11
SF = {V} implies meet SF = V
proof
assume
A1: SF = {V};
now
let i be object;
assume
A2: i in I;
then consider Q be Subset-Family of (M.i) such that
A3: Q = SF.i and
A4: (meet SF).i = Intersect Q by Def1;
thus (meet SF).i = meet Q by A1,A2,A3,A4,SETFAM_1:def 9
.= meet {V.i} by A1,A2,A3,PZFMISC1:def 1
.= V.i by SETFAM_1:10;
end;
hence thesis;
end;
theorem Th51: :: SETFAM_1:12
SF = { V,W } implies meet SF = V (/\) W
proof
assume
A1: SF = { V,W };
now
let i be object;
assume
A2: i in I;
then
ex Q be Subset-Family of (M.i) st Q = SF.i & (meet SF).i = Intersect Q
by Def1;
hence (meet SF).i = meet ({V,W}.i) by A1,A2,SETFAM_1:def 9
.= meet {V.i,W.i} by A2,PZFMISC1:def 2
.= V.i /\ W.i by SETFAM_1:11
.= (V (/\) W).i by A2,PBOOLE:def 5;
end;
hence thesis;
end;
theorem
A in meet SF implies for B st B in SF holds A in B
proof
assume
A1: A in meet SF;
let B such that
A2: B in SF;
let i be object;
assume
A3: i in I;
then
A4: A.i in (meet SF).i by A1;
A5: B.i in SF.i by A2,A3;
ex Q be Subset-Family of (M.i) st Q = SF.i & (meet SF).i = Intersect Q by A3
,Def1;
hence thesis by A4,A5,SETFAM_1:43;
end;
theorem
for A, M be ManySortedSet of I for SF be non-empty MSSubsetFamily of M
st (A in M & for B be ManySortedSet of I st B in SF holds A in B) holds A in
meet SF
proof
let A, M be ManySortedSet of I, SF be non-empty MSSubsetFamily of M;
assume that
A1: A in M and
A2: for B be ManySortedSet of I st B in SF holds A in B;
let i be object;
consider T be ManySortedSet of I such that
A3: T in SF by PBOOLE:134;
assume
A4: i in I;
then consider Q be Subset-Family of (M.i) such that
A5: Q = SF.i and
A6: (meet SF).i = Intersect Q by Def1;
A7: for B9 be set st B9 in Q holds A.i in B9
proof
let B9 be set such that
A8: B9 in Q;
dom (T +* (i .--> B9)) = I by A4,PZFMISC1:1;
then reconsider K = T +* (i .--> B9) as ManySortedSet of I by
PARTFUN1:def 2,RELAT_1:def 18;
A9: dom (i .--> B9) = {i};
i in {i} by TARSKI:def 1;
then
A10: K.i = (i .--> B9).i by A9,FUNCT_4:13
.= B9 by FUNCOP_1:72;
K in SF
proof
let q be object such that
A11: q in I;
per cases;
suppose
q = i;
hence thesis by A5,A8,A10;
end;
suppose
q <> i;
then not q in dom (i .--> B9) by TARSKI:def 1;
then K.q = T.q by FUNCT_4:11;
hence thesis by A3,A11;
end;
end;
then A in K by A2;
hence thesis by A4,A10;
end;
A.i in M.i by A1,A4;
hence thesis by A6,A7,SETFAM_1:43;
end;
definition
let I, M;
let IT be MSSubsetFamily of M;
attr IT is additive means
for A, B st A in IT & B in IT holds A (\/) B in IT;
attr IT is absolutely-additive means
for F be MSSubsetFamily of M st F c= IT holds union F in IT;
attr IT is multiplicative means
for A, B st A in IT & B in IT holds A (/\) B in IT;
attr IT is absolutely-multiplicative means
for F be MSSubsetFamily of M st F c= IT holds meet F in IT;
attr IT is properly-upper-bound means
M in IT;
attr IT is properly-lower-bound means
EmptyMS I in IT;
end;
Lm1: bool M is additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound
proof
thus bool M is additive
proof
let A, B;
assume A in bool M & B in bool M;
then A c= M & B c= M by MBOOLEAN:1;
then A (\/) B c= M by PBOOLE:16;
hence A (\/)B in bool M by MBOOLEAN:1;
end;
thus bool M is absolutely-additive
by Th40,MBOOLEAN:18;
thus bool M is multiplicative
proof
let A, B;
assume that
A1: A in bool M and
B in bool M;
A c= M by A1,MBOOLEAN:1;
then A (/\) B c= M by MBOOLEAN:14;
hence thesis by MBOOLEAN:1;
end;
thus bool M is absolutely-multiplicative
by PBOOLE:def 18,MBOOLEAN:18;
M in bool M by MBOOLEAN:18;
hence bool M is properly-upper-bound;
EmptyMS I c= M by MBOOLEAN:5;
then EmptyMS I in bool M by MBOOLEAN:1;
hence bool M is properly-lower-bound;
end;
registration
let I, M;
cluster non-empty additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound
for MSSubsetFamily of M;
existence
proof
take bool M;
thus thesis by Lm1;
end;
end;
definition
let I, M;
redefine func bool M -> additive absolutely-additive multiplicative :: redefines bool (MBOOLEAN, definition)
absolutely-multiplicative properly-upper-bound properly-lower-bound
MSSubsetFamily of M;
coherence by Lm1;
end;
registration
let I, M;
cluster absolutely-additive -> additive for MSSubsetFamily of M;
coherence
proof
let SF be MSSubsetFamily of M such that
A1: SF is absolutely-additive;
let A, B;
assume that
A2: A in SF and
A3: B in SF;
{A} c= SF & {B} c= SF by A2,A3,PZFMISC1:33;
then {A} (\/) {B} c= SF by PBOOLE:16;
then
A4: {A,B} c= SF by PZFMISC1:10;
B is ManySortedSubset of M by A3,Th33;
then
A5: B c= M by PBOOLE:def 18;
A is ManySortedSubset of M by A2,Th33;
then A c= M by PBOOLE:def 18;
then {A,B} is MSSubsetFamily of M by A5,Th39;
then union {A,B} in SF by A1,A4;
hence thesis by PZFMISC1:32;
end;
end;
registration
let I, M;
cluster absolutely-multiplicative -> multiplicative for MSSubsetFamily of M;
coherence
proof
let SF be MSSubsetFamily of M such that
A1: SF is absolutely-multiplicative;
let A, B;
assume that
A2: A in SF and
A3: B in SF;
A4: B is ManySortedSubset of M by A3,Th33;
then
A5: B c= M by PBOOLE:def 18;
A6: A is ManySortedSubset of M by A2,Th33;
then A c= M by PBOOLE:def 18;
then reconsider ab = {A,B} as MSSubsetFamily of M by A5,Th39;
{A} c= SF & {B} c= SF by A2,A3,PZFMISC1:33;
then {A} (\/) {B} c= SF by PBOOLE:16;
then {A,B} c= SF by PZFMISC1:10;
then meet ab in SF by A1;
hence thesis by A6,A4,Th51;
end;
end;
registration
let I, M;
cluster absolutely-multiplicative -> properly-upper-bound
for MSSubsetFamily of M;
coherence
proof
EmptyMS I c= bool M by PBOOLE:43;
then reconsider a = EmptyMS I as MSSubsetFamily of M by PBOOLE:def 18;
let SF be MSSubsetFamily of M such that
A1: SF is absolutely-multiplicative;
meet a = M & EmptyMS I c= SF by Th41,PBOOLE:43;
hence M in SF by A1;
end;
end;
registration
let I, M;
cluster properly-upper-bound -> non-empty for MSSubsetFamily of M;
coherence
proof
let SF be MSSubsetFamily of M;
assume SF is properly-upper-bound;
then
A1: M in SF;
let i be object;
assume i in I;
hence thesis by A1;
end;
end;
registration
let I, M;
cluster absolutely-additive -> properly-lower-bound for MSSubsetFamily of M;
coherence
proof
EmptyMS I c= bool M by PBOOLE:43;
then reconsider a = EmptyMS I as MSSubsetFamily of M by PBOOLE:def 18;
let SF be MSSubsetFamily of M such that
A1: SF is absolutely-additive;
union a = EmptyMS I & EmptyMS I c= SF by PBOOLE:43;
hence EmptyMS I in SF by A1;
end;
end;
registration
let I, M;
cluster properly-lower-bound -> non-empty for MSSubsetFamily of M;
coherence
proof
let SF be MSSubsetFamily of M;
assume SF is properly-lower-bound;
then
A1: EmptyMS I in SF;
let i be object;
assume i in I;
hence thesis by A1;
end;
end;