Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Properties of Subsets

**by****Zinaida Trybulec**- Received March 4, 1989
- MML identifier: SUBSET_1

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, SUBSET_1, NEWTON; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1; constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1; clusters XBOOLE_0; requirements BOOLE; begin reserve E,X,x,y for set; definition let X be set; cluster bool X -> non empty; end; definition let x; cluster { x } -> non empty; let y; cluster { x, y } -> non empty; end; definition let X; canceled; mode Element of X means :: SUBSET_1:def 2 it in X if X is non empty otherwise it is empty; end; definition let X; mode Subset of X is Element of bool X; end; definition let X be non empty set; cluster non empty Subset of X; end; definition let X1,X2 be non empty set; cluster [: X1,X2 :] -> non empty; end; definition let X1,X2,X3 be non empty set; cluster [: X1,X2,X3 :] -> non empty; end; definition let X1,X2,X3,X4 be non empty set; cluster [: X1,X2,X3,X4 :] -> non empty; end; definition let D be non empty set, X be non empty Subset of D; redefine mode Element of X -> Element of D; end; definition let E; cluster empty Subset of E; end; definition let E; func {} E -> empty Subset of E equals :: SUBSET_1:def 3 {}; func [#] E -> Subset of E equals :: SUBSET_1:def 4 E; end; canceled 3; theorem :: SUBSET_1:4 {} is Subset of X; reserve A,B,C for Subset of E; canceled 2; theorem :: SUBSET_1:7 (for x being Element of E holds x in A implies x in B) implies A c= B; theorem :: SUBSET_1:8 (for x being Element of E holds x in A iff x in B) implies A = B; canceled; theorem :: SUBSET_1:10 A <> {} implies ex x being Element of E st x in A; definition let E,A; func A` -> Subset of E equals :: SUBSET_1:def 5 E \ A; involutiveness; let B; redefine func A \/ B -> Subset of E; func A /\ B -> Subset of E; func A \ B -> Subset of E; func A \+\ B -> Subset of E; end; canceled 4; theorem :: SUBSET_1:15 (for x being Element of E holds x in A iff x in B or x in C) implies A = B \/ C; theorem :: SUBSET_1:16 (for x being Element of E holds x in A iff x in B & x in C) implies A = B /\ C; theorem :: SUBSET_1:17 (for x being Element of E holds x in A iff x in B & not x in C) implies A = B \ C; theorem :: SUBSET_1:18 (for x being Element of E holds x in A iff not(x in B iff x in C)) implies A = B \+\ C; canceled 2; theorem :: SUBSET_1:21 {} E = ([#] E)`; theorem :: SUBSET_1:22 [#] E = ({} E)`; canceled 2; theorem :: SUBSET_1:25 A \/ A` = [#]E; theorem :: SUBSET_1:26 A misses A`; canceled; theorem :: SUBSET_1:28 A \/ [#]E = [#]E; theorem :: SUBSET_1:29 (A \/ B)` = A` /\ B`; theorem :: SUBSET_1:30 (A /\ B)` = A` \/ B`; theorem :: SUBSET_1:31 A c= B iff B` c= A`; theorem :: SUBSET_1:32 A \ B = A /\ B`; theorem :: SUBSET_1:33 (A \ B)` = A` \/ B; theorem :: SUBSET_1:34 (A \+\ B)` = A /\ B \/ A` /\ B`; theorem :: SUBSET_1:35 A c= B` implies B c= A`; theorem :: SUBSET_1:36 A` c= B implies B` c= A; canceled; theorem :: SUBSET_1:38 A c= A` iff A = {}E; theorem :: SUBSET_1:39 A` c= A iff A = [#]E; theorem :: SUBSET_1:40 X c= A & X c= A` implies X = {}; theorem :: SUBSET_1:41 (A \/ B)` c= A`; theorem :: SUBSET_1:42 A` c= (A /\ B)`; theorem :: SUBSET_1:43 A misses B iff A c= B`; theorem :: SUBSET_1:44 A misses B` iff A c= B; canceled; theorem :: SUBSET_1:46 A misses B & A` misses B` implies A = B`; theorem :: SUBSET_1:47 A c= B & C misses B implies A c= C`; :: :: ADDITIONAL THEOREMS :: theorem :: SUBSET_1:48 (for a being Element of A holds a in B) implies A c= B; theorem :: SUBSET_1:49 (for x being Element of E holds x in A) implies E = A; theorem :: SUBSET_1:50 E <> {} implies for B for x being Element of E st not x in B holds x in B`; theorem :: SUBSET_1:51 for A,B st for x being Element of E holds x in A iff not x in B holds A = B`; theorem :: SUBSET_1:52 for A,B st for x being Element of E holds not x in A iff x in B holds A = B`; theorem :: SUBSET_1:53 for A,B st for x being Element of E holds not(x in A iff x in B) holds A = B`; theorem :: SUBSET_1:54 x in A` implies not x in A; reserve x1,x2,x3,x4,x5,x6,x7,x8 for Element of X; theorem :: SUBSET_1:55 X <> {} implies {x1} is Subset of X; theorem :: SUBSET_1:56 X <> {} implies {x1,x2} is Subset of X; theorem :: SUBSET_1:57 X <> {} implies {x1,x2,x3} is Subset of X; theorem :: SUBSET_1:58 X <> {} implies {x1,x2,x3,x4} is Subset of X; theorem :: SUBSET_1:59 X <> {} implies {x1,x2,x3,x4,x5} is Subset of X; theorem :: SUBSET_1:60 X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X; theorem :: SUBSET_1:61 X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X; theorem :: SUBSET_1:62 X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X; theorem :: SUBSET_1:63 x in X implies {x} is Subset of X; scheme Subset_Ex { A()-> set, P[set] } : ex X being Subset of A() st for x holds x in X iff x in A() & P[x]; scheme Subset_Eq {X() -> set, P[set]}: for X1,X2 being Subset of X() st (for y being Element of X() holds y in X1 iff P[y]) & (for y being Element of X() holds y in X2 iff P[y]) holds X1 = X2; definition let X, Y be non empty set; redefine pred X misses Y; irreflexivity; antonym X meets Y; end; definition let S be set; assume contradiction; func choose S -> Element of S means :: SUBSET_1:def 6 not contradiction; end;

Back to top