:: Families of Sets
:: by Beata Padlewska
::
:: Received April 5, 1989
:: Copyright (c) 1990-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, TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1;
constructors TARSKI, ENUMSET1, SUBSET_1;
registrations XBOOLE_0, SUBSET_1;
requirements SUBSET, BOOLE;
begin
reserve X,Y,Z,Z1,Z2,D for set,x,y for object;
definition
let X;
func meet X -> set means
:: SETFAM_1:def 1
for x being object holds x in it iff
for Y holds Y in X implies x in Y if X <> {}
otherwise it = {};
end;
:: Intersection of families of sets
theorem :: SETFAM_1:1
meet {} = {};
theorem :: SETFAM_1:2
meet X c= union X;
theorem :: SETFAM_1:3
Z in X implies meet X c= Z;
theorem :: SETFAM_1:4
{} in X implies meet X = {};
theorem :: SETFAM_1:5
X <> {} & (for Z1 st Z1 in X holds Z c= Z1) implies Z c= meet X;
theorem :: SETFAM_1:6
X <> {} & X c= Y implies meet Y c= meet X;
theorem :: SETFAM_1:7
X in Y & X c= Z implies meet Y c= Z;
theorem :: SETFAM_1:8
X in Y & X misses Z implies meet Y misses Z;
theorem :: SETFAM_1:9
X <> {} & Y <> {} implies meet (X \/ Y) = meet X /\ meet Y;
theorem :: SETFAM_1:10
meet {X} = X;
theorem :: SETFAM_1:11
meet {X,Y} = X /\ Y;
reserve SFX,SFY,SFZ for set;
definition
let SFX,SFY;
pred SFX is_finer_than SFY means
:: SETFAM_1:def 2
for X st X in SFX ex Y st Y in SFY & X c= Y;
reflexivity;
pred SFY is_coarser_than SFX means
:: SETFAM_1:def 3
for Y st Y in SFY ex X st X in SFX & X c= Y;
reflexivity;
end;
theorem :: SETFAM_1:12
SFX c= SFY implies SFX is_finer_than SFY;
theorem :: SETFAM_1:13
SFX is_finer_than SFY implies union SFX c= union SFY;
theorem :: SETFAM_1:14
SFY <> {} & SFY is_coarser_than SFX implies meet SFX c= meet SFY;
theorem :: SETFAM_1:15
{} is_finer_than SFX;
theorem :: SETFAM_1:16
SFX is_finer_than {} implies SFX = {};
theorem :: SETFAM_1:17
SFX is_finer_than SFY & SFY is_finer_than SFZ implies SFX is_finer_than SFZ;
theorem :: SETFAM_1:18
SFX is_finer_than {Y} implies for X st X in SFX holds X c= Y;
theorem :: SETFAM_1:19
SFX is_finer_than {X,Y} implies for Z st Z in SFX holds Z c= X or Z c= Y;
definition
let SFX,SFY;
func UNION (SFX,SFY) -> set means
:: SETFAM_1:def 4
Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X \/ Y;
commutativity;
func INTERSECTION (SFX,SFY) -> set means
:: SETFAM_1:def 5
Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X /\ Y;
commutativity;
func DIFFERENCE (SFX,SFY) -> set means
:: SETFAM_1:def 6
Z in it iff ex X,Y st X in SFX & Y in SFY & Z = X \ Y;
end;
theorem :: SETFAM_1:20
SFX is_finer_than UNION(SFX,SFX);
theorem :: SETFAM_1:21
INTERSECTION(SFX,SFX) is_finer_than SFX;
theorem :: SETFAM_1:22
DIFFERENCE(SFX,SFX) is_finer_than SFX;
theorem :: SETFAM_1:23
SFX meets SFY implies meet SFX /\ meet SFY = meet INTERSECTION(SFX,SFY );
theorem :: SETFAM_1:24
SFY <> {} implies X \/ meet SFY = meet UNION({X},SFY);
theorem :: SETFAM_1:25
X /\ union SFY = union INTERSECTION({X},SFY);
theorem :: SETFAM_1:26
SFY <> {} implies X \ union SFY = meet DIFFERENCE({X},SFY);
theorem :: SETFAM_1:27
SFY <> {} implies X \ meet SFY = union DIFFERENCE ({X},SFY);
theorem :: SETFAM_1:28
union INTERSECTION (SFX,SFY) = union SFX /\ union SFY;
theorem :: SETFAM_1:29
SFX <> {} & SFY <> {} implies meet SFX \/ meet SFY c= meet UNION (SFX, SFY);
theorem :: SETFAM_1:30
meet DIFFERENCE (SFX,SFY) c= meet SFX \ meet SFY;
:: Family of subsets of a set
definition
let D be set;
mode Subset-Family of D is Subset of bool D;
end;
reserve F,G for Subset-Family of D;
reserve P for Subset of D;
definition
let D,F;
redefine func union F -> Subset of D;
end;
definition
let D,F;
redefine func meet F -> Subset of D;
end;
theorem :: SETFAM_1:31
(for P holds P in F iff P in G) implies F=G;
definition
let D,F;
func COMPLEMENT(F) -> Subset-Family of D means
:: SETFAM_1:def 7
for P being Subset of D holds P in it iff P` in F;
involutiveness;
end;
theorem :: SETFAM_1:32
F <> {} implies COMPLEMENT(F) <> {};
theorem :: SETFAM_1:33
F <> {} implies [#] D \ union F = meet (COMPLEMENT(F));
theorem :: SETFAM_1:34
F <> {} implies union COMPLEMENT(F) = [#] D \ meet F;
begin :: Addendum
:: from YELLOW_8, 2004.07.25
theorem :: SETFAM_1:35
for X being set, F being Subset-Family of X for P being Subset of X
holds P` in COMPLEMENT F iff P in F;
theorem :: SETFAM_1:36
for X being set, F,G being Subset-Family of X st COMPLEMENT F c=
COMPLEMENT G holds F c= G;
theorem :: SETFAM_1:37
for X being set, F,G being Subset-Family of X holds COMPLEMENT F c= G
iff F c= COMPLEMENT G;
theorem :: SETFAM_1:38
for X being set, F,G being Subset-Family of X st COMPLEMENT F =
COMPLEMENT G holds F = G;
theorem :: SETFAM_1:39
for X being set, F,G being Subset-Family of X holds COMPLEMENT(F \/ G)
= COMPLEMENT F \/ COMPLEMENT G;
theorem :: SETFAM_1:40
for X being set, F being Subset-Family of X st F = {X} holds
COMPLEMENT F = {{}};
registration
let X be set, F be empty Subset-Family of X;
cluster COMPLEMENT F -> empty;
end;
:: from AMI_1
definition
let IT be set;
attr IT is with_non-empty_elements means
:: SETFAM_1:def 8
not {} in IT;
end;
registration
cluster non empty with_non-empty_elements for set;
end;
registration
let A be non empty set;
cluster { A } -> with_non-empty_elements;
let B be non empty set;
cluster { A, B } -> with_non-empty_elements;
let C be non empty set;
cluster { A, B, C } -> with_non-empty_elements;
let D be non empty set;
cluster { A, B, C, D } -> with_non-empty_elements;
let E be non empty set;
cluster { A, B, C, D, E } -> with_non-empty_elements;
let F be non empty set;
cluster { A, B, C, D, E, F } -> with_non-empty_elements;
let G be non empty set;
cluster { A, B, C, D, E, F, G } -> with_non-empty_elements;
let H be non empty set;
cluster { A, B, C, D, E, F, G, H } -> with_non-empty_elements;
let I be non empty set;
cluster { A, B, C, D, E, F, G, H, I } -> with_non-empty_elements;
let J be non empty set;
cluster { A, B, C, D, E, F, G, H, I, J } -> with_non-empty_elements;
end;
registration
let A,B be with_non-empty_elements set;
cluster A \/ B -> with_non-empty_elements;
end;
:: from LATTICE4
theorem :: SETFAM_1:41
union Y c= Z & X in Y implies X c= Z;
:: from LOPCLSET
theorem :: SETFAM_1:42
for A,B,X being set holds ( X c= union (A \/ B) & for Y being set st Y
in B holds Y misses X ) implies X c= union A;
:: from CANTOR_1
definition
let M be set;
let B be Subset-Family of M;
func Intersect B -> Subset of M equals
:: SETFAM_1:def 9
meet B if B <> {} otherwise M;
end;
theorem :: SETFAM_1:43
for X, x being set, R being Subset-Family of X st x in X holds x
in Intersect R iff for Y being set st Y in R holds x in Y;
theorem :: SETFAM_1:44
for X being set for H, J being Subset-Family of X st H c= J holds
Intersect J c= Intersect H;
:: from PUA2MSS1, 2005.08.22, A.T
registration
let X be non empty with_non-empty_elements set;
cluster -> non empty for Element of X;
end;
:: from ABIAN, 2005.08.22, A.T
reserve E for set;
definition
let E;
attr E is empty-membered means
:: SETFAM_1:def 10
not ex x being non empty set st x in E;
end;
notation
let E;
antonym E is with_non-empty_element for E is empty-membered;
end;
registration
cluster with_non-empty_element for set;
end;
registration
cluster with_non-empty_element -> non empty for set;
end;
:: from TRIANG_1, 2005.08.22
registration
let X be with_non-empty_element set;
cluster non empty for Element of X;
end;
:: from MSAFREE1, 2007.03.09, A.T.
registration
let D be non empty with_non-empty_elements set;
cluster union D -> non empty;
end;
:: missing, 2007.03.09, A.T.
registration
cluster non empty with_non-empty_elements -> with_non-empty_element for set;
end;
:: the concept of a cover, 2008.03.08, A.T.
definition
let X be set;
mode Cover of X -> set means
:: SETFAM_1:def 11
X c= union it;
end;
theorem :: SETFAM_1:45
for X being set, F being Subset-Family of X holds F is Cover of X iff
union F = X;
:: from MEASURE1, 2008.06.08, A.T.
theorem :: SETFAM_1:46
{{}} is Subset-Family of X;
:: from BORSUK_5 (generalized), 2008.06.08, A.T.
definition
let X be set;
let F be Subset-Family of X;
attr F is with_proper_subsets means
:: SETFAM_1:def 12
not X in F;
end;
theorem :: SETFAM_1:47
for TS being set, F, G being Subset-Family of TS st F is
with_proper_subsets & G c= F holds G is with_proper_subsets;
registration
let TS be non empty set;
cluster with_proper_subsets for Subset-Family of TS;
end;
theorem :: SETFAM_1:48
for TS being non empty set, A, B being with_proper_subsets
Subset-Family of TS holds A \/ B is with_proper_subsets;
:: from YELLOW21, 2008.09.10, A.T.
registration
cluster non trivial -> with_non-empty_element for set;
end;
:: from PCOMPS_1, 2010.02.26, A.T.
definition
let X be set;
redefine func bool X -> Subset-Family of X;
end;
:: from HAHNBAN, 2011.04.26., A.T.
theorem :: SETFAM_1:49
for A being non empty set, b being object st A <> {b}
ex a being Element of A st a <> b;