:: Certain Facts about Families of Subsets of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received October 27, 1995
:: Copyright (c) 1995-2018 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;
begin :: Preliminaries
registration
let I be set;
let F be ManySortedFunction of I;
cluster doms F -> I-defined;
cluster rngs F -> I-defined;
end;
registration
let I be set;
let F be ManySortedFunction of I;
cluster doms F -> total for I-defined Function;
cluster rngs F -> total for I-defined Function;
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 :: MSSUBFAM:sch 1
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
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];
theorem :: MSSUBFAM:1 :: SETFAM_1:3
sf <> {} implies Intersect sf c= union sf;
theorem :: MSSUBFAM:2 :: SETFAM_1:4
G in sf implies Intersect sf c= G;
theorem :: MSSUBFAM:3 :: SETFAM_1:5
{} in sf implies Intersect sf = {};
theorem :: MSSUBFAM:4 :: 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;
theorem :: MSSUBFAM:5 :: SETFAM_1:6
sf <> {} & (for Z1 be set st Z1 in sf holds G c= Z1) implies G c=
Intersect sf;
theorem :: MSSUBFAM:6 :: SETFAM_1:8
G in sf & G c= H implies Intersect sf c= H;
theorem :: MSSUBFAM:7 :: SETFAM_1:9
G in sf & G misses H implies Intersect sf misses H;
theorem :: MSSUBFAM:8 :: SETFAM_1:10
sh = sf \/ sg implies Intersect sh = Intersect sf /\ Intersect sg;
theorem :: MSSUBFAM:9 :: SETFAM_1:11
sf = {v} implies Intersect sf = v;
theorem :: MSSUBFAM:10 :: SETFAM_1:12
sf = { v,w } implies Intersect sf = v /\ w;
theorem :: MSSUBFAM:11
A in B implies A is Element of B;
theorem :: MSSUBFAM:12
for B be non-empty ManySortedSet of I holds A is Element of B implies A in B;
theorem :: MSSUBFAM:13
for f be Function st i in I & f = F.i holds (rngs F).i = rng f;
theorem :: MSSUBFAM:14
for f be Function st i in I & f = F.i holds (doms F).i = dom f;
theorem :: MSSUBFAM:15
for F, G be ManySortedFunction of I holds G ** F is ManySortedFunction of I;
theorem :: MSSUBFAM:16
for A be non-empty ManySortedSet of I for F be ManySortedFunction of A
, EmptyMS I holds F = EmptyMS I;
theorem :: MSSUBFAM:17
A is_transformable_to B & F is ManySortedFunction of A, B implies
doms F = A & rngs F c= B;
begin :: Finite Many Sorted Sets
registration
let I;
cluster empty-yielding -> finite-yielding for ManySortedSet of I;
end;
registration
let I;
cluster EmptyMS I -> empty-yielding finite-yielding;
end;
registration
let I, A;
cluster empty-yielding finite-yielding for ManySortedSubset of A;
end;
theorem :: MSSUBFAM:18
A c= B & B is finite-yielding implies A is finite-yielding;
registration
let I;
let A be finite-yielding ManySortedSet of I;
cluster -> finite-yielding for ManySortedSubset of A;
end;
registration
let I;
let A, B be finite-yielding ManySortedSet of I;
cluster A (\/) B -> finite-yielding;
end;
registration
let I, A;
let B be finite-yielding ManySortedSet of I;
cluster A (/\) B -> finite-yielding;
end;
registration
let I, B;
let A be finite-yielding ManySortedSet of I;
cluster A (/\) B -> finite-yielding;
end;
registration
let I, B;
let A be finite-yielding ManySortedSet of I;
cluster A (\) B -> finite-yielding;
end;
registration
let I, F;
let A be finite-yielding ManySortedSet of I;
cluster F.:.:A -> finite-yielding;
end;
registration
let I;
let A, B be finite-yielding ManySortedSet of I;
cluster [|A,B|] -> finite-yielding;
end;
theorem :: MSSUBFAM:19 :: FINSET_1:22
B is non-empty & [|A,B|] is finite-yielding implies A is finite-yielding;
theorem :: MSSUBFAM:20 :: FINSET_1:23
A is non-empty & [|A,B|] is finite-yielding implies B is finite-yielding;
theorem :: MSSUBFAM:21
A is finite-yielding iff bool A is finite-yielding;
registration
let I;
let M be finite-yielding ManySortedSet of I;
cluster bool M -> finite-yielding;
end;
theorem :: MSSUBFAM:22
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;
theorem :: MSSUBFAM:23
union A is finite-yielding implies A is finite-yielding & for M st M
in A holds M is finite-yielding;
theorem :: MSSUBFAM:24 :: FINSET_1:26
doms F is finite-yielding implies rngs F is finite-yielding;
theorem :: MSSUBFAM:25 :: 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;
registration
let I;
let A, B be finite-yielding ManySortedSet of I;
cluster (Funcs)(A,B) -> finite-yielding;
end;
registration
let I;
let A, B be finite-yielding ManySortedSet of I;
cluster A (\+\) B -> finite-yielding;
end;
reserve X, Y, Z for ManySortedSet of I;
theorem :: MSSUBFAM:26 :: 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|];
theorem :: MSSUBFAM:27 :: 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|];
theorem :: MSSUBFAM:28
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;
theorem :: MSSUBFAM:29 :: 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;
theorem :: MSSUBFAM:30 :: 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;
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;
end;
definition
let I, M;
redefine func bool M -> MSSubsetFamily of M;
end;
registration
let I, M;
cluster empty-yielding finite-yielding for MSSubsetFamily of M;
end;
theorem :: MSSUBFAM:31
EmptyMS I is empty-yielding finite-yielding MSSubsetFamily of M;
registration
let I;
let M be finite-yielding ManySortedSet of I;
cluster non-empty finite-yielding for MSSubsetFamily of M;
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);
end;
theorem :: MSSUBFAM:32
i in I implies SF.i is Subset-Family of (M.i);
theorem :: MSSUBFAM:33
A in SF implies A is ManySortedSubset of M;
theorem :: MSSUBFAM:34
SF (\/) SG is MSSubsetFamily of M;
theorem :: MSSUBFAM:35
SF (/\) SG is MSSubsetFamily of M;
theorem :: MSSUBFAM:36
SF (\) A is MSSubsetFamily of M;
theorem :: MSSUBFAM:37
SF (\+\) SG is MSSubsetFamily of M;
theorem :: MSSUBFAM:38
A c= M implies {A} is MSSubsetFamily of M;
theorem :: MSSUBFAM:39
A c= M & B c= M implies {A,B} is MSSubsetFamily of M;
theorem :: MSSUBFAM:40
union SF c= M;
begin :: Intersection of a Family of Many Sorted Sets
definition
let I, M, SF;
func meet SF -> ManySortedSet of I means
:: MSSUBFAM:def 1
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;
end;
definition
let I, M, SF;
redefine func meet SF -> ManySortedSubset of M;
end;
theorem :: MSSUBFAM:41
SF = EmptyMS I implies meet SF = M;
theorem :: MSSUBFAM:42 :: SETFAM_1:3
meet SFe c= union SFe;
theorem :: MSSUBFAM:43 :: SETFAM_1:4
A in SF implies meet SF c= A;
theorem :: MSSUBFAM:44 :: SETFAM_1:5
EmptyMS I in SF implies meet SF = EmptyMS I;
theorem :: MSSUBFAM:45 :: 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;
theorem :: MSSUBFAM:46 :: SETFAM_1:7 :: SETFAM_1:59
SF c= SG implies meet SG c= meet SF;
theorem :: MSSUBFAM:47 :: SETFAM_1:8
A in SF & A c= B implies meet SF c= B;
theorem :: MSSUBFAM:48 :: SETFAM_1:9
A in SF & A (/\) B = EmptyMS I implies meet SF (/\) B = EmptyMS I;
theorem :: MSSUBFAM:49 :: SETFAM_1:10
SH = SF (\/) SG implies meet SH = meet SF (/\) meet SG;
theorem :: MSSUBFAM:50 :: SETFAM_1:11
SF = {V} implies meet SF = V;
theorem :: MSSUBFAM:51 :: SETFAM_1:12
SF = { V,W } implies meet SF = V (/\) W;
theorem :: MSSUBFAM:52
A in meet SF implies for B st B in SF holds A in B;
theorem :: MSSUBFAM:53
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;
definition
let I, M;
let IT be MSSubsetFamily of M;
attr IT is additive means
:: MSSUBFAM:def 2
for A, B st A in IT & B in IT holds A (\/) B in IT;
attr IT is absolutely-additive means
:: MSSUBFAM:def 3
for F be MSSubsetFamily of M st F c= IT holds union F in IT;
attr IT is multiplicative means
:: MSSUBFAM:def 4
for A, B st A in IT & B in IT holds A (/\) B in IT;
attr IT is absolutely-multiplicative means
:: MSSUBFAM:def 5
for F be MSSubsetFamily of M st F c= IT holds meet F in IT;
attr IT is properly-upper-bound means
:: MSSUBFAM:def 6
M in IT;
attr IT is properly-lower-bound means
:: MSSUBFAM:def 7
EmptyMS I in IT;
end;
registration
let I, M;
cluster non-empty additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound
for MSSubsetFamily of M;
end;
definition
let I, M;
redefine func bool M -> additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound
MSSubsetFamily of M;
end;
registration
let I, M;
cluster absolutely-additive -> additive for MSSubsetFamily of M;
end;
registration
let I, M;
cluster absolutely-multiplicative -> multiplicative for MSSubsetFamily of M;
end;
registration
let I, M;
cluster absolutely-multiplicative -> properly-upper-bound
for MSSubsetFamily of M;
end;
registration
let I, M;
cluster properly-upper-bound -> non-empty for MSSubsetFamily of M;
end;
registration
let I, M;
cluster absolutely-additive -> properly-lower-bound for MSSubsetFamily of M;
end;
registration
let I, M;
cluster properly-lower-bound -> non-empty for MSSubsetFamily of M;
end;