:: Properties of Subsets
:: by Zinaida Trybulec
::
:: Received March 4, 1989
:: Copyright (c) 1990-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 ZFMISC_1, XBOOLE_0, TARSKI, SUBSET_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
constructors TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1;
registrations XBOOLE_0, ZFMISC_1;
requirements BOOLE;
begin
reserve E,X,Y,x,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 for set;
registration
let X be set;
cluster bool X -> non empty;
end;
registration
let x1, x2, x3 be object;
cluster { x1, x2, x3 } -> non empty;
let x4 be object;
cluster { x1, x2, x3, x4 } -> non empty;
let x5 be object;
cluster { x1, x2, x3, x4, x5 } -> non empty;
let x6 be object;
cluster { x1, x2, x3, x4, x5, x6 } -> non empty;
let x7 be object;
cluster { x1, x2, x3, x4, x5, x6, x7 } -> non empty;
let x8 be object;
cluster { x1, x2, x3, x4, x5, x6, x7, x8 } -> non empty;
let x9 be object;
cluster { x1, x2, x3, x4, x5, x6, x7, x8, x9 } -> non empty;
let x10 be object;
cluster { x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 } -> non empty;
end;
definition
let X;
mode Element of X -> set means
:: SUBSET_1:def 1
it in X if X is non empty otherwise it is empty;
sethood;
end;
definition
let X;
mode Subset of X is Element of bool X;
end;
registration
let X be non empty set;
cluster non empty for Subset of X;
end;
registration
let X1,X2 be non empty set;
cluster [: X1,X2 :] -> non empty;
end;
registration
let X1,X2,X3 be non empty set;
cluster [: X1,X2,X3 :] -> non empty;
end;
registration
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;
registration
let E;
cluster empty for Subset of E;
end;
definition
let E;
func {}E -> Subset of E equals
:: SUBSET_1:def 2
{};
func [#] E -> Subset of E equals
:: SUBSET_1:def 3
E;
end;
registration
let E;
cluster {}E -> empty;
end;
theorem :: SUBSET_1:1
{} is Subset of X;
reserve A,B,C for Subset of E;
theorem :: SUBSET_1:2
(for x being Element of E holds x in A implies x in B) implies A c= B;
theorem :: SUBSET_1:3
(for x being Element of E holds x in A iff x in B) implies A = B;
theorem :: SUBSET_1:4
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 4
E \ A;
involutiveness;
let B;
redefine func A \/ B -> Subset of E;
redefine func A \+\ B -> Subset of E;
end;
definition
let X,Y be set;
redefine func X \ Y -> Subset of X;
end;
definition
let E,A,X;
redefine func A \ X -> Subset of E;
end;
definition
let E,A,X;
redefine func A /\ X -> Subset of E;
end;
definition
let E,X,A;
redefine func X /\ A -> Subset of E;
end;
theorem :: SUBSET_1:5
(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:6
(for x being Element of E holds x in A iff x in B & x in C) implies A
= B /\ C;
theorem :: SUBSET_1:7
(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:8
(for x being Element of E holds x in A iff not(x in B iff x in C))
implies A = B \+\ C;
theorem :: SUBSET_1:9
[#] E = ({} E)`;
theorem :: SUBSET_1:10
A \/ A` = [#]E;
theorem :: SUBSET_1:11
A \/ [#]E = [#]E;
theorem :: SUBSET_1:12
A c= B iff B` c= A`;
theorem :: SUBSET_1:13
A \ B = A /\ B`;
theorem :: SUBSET_1:14
(A \ B)` = A` \/ B;
theorem :: SUBSET_1:15
(A \+\ B)` = A /\ B \/ A` /\ B`;
theorem :: SUBSET_1:16
A c= B` implies B c= A`;
theorem :: SUBSET_1:17
A` c= B implies B` c= A;
theorem :: SUBSET_1:18
A c= A` iff A = {}E;
theorem :: SUBSET_1:19
A` c= A iff A = [#]E;
theorem :: SUBSET_1:20
X c= A & X c= A` implies X = {};
theorem :: SUBSET_1:21
(A \/ B)` c= A`;
theorem :: SUBSET_1:22
A` c= (A /\ B)`;
theorem :: SUBSET_1:23
A misses B iff A c= B`;
theorem :: SUBSET_1:24
A misses B` iff A c= B;
theorem :: SUBSET_1:25
A misses B & A` misses B` implies A = B`;
theorem :: SUBSET_1:26
A c= B & C misses B implies A c= C`;
::
:: ADDITIONAL THEOREMS
::
theorem :: SUBSET_1:27
(for a being Element of A holds a in B) implies A c= B;
theorem :: SUBSET_1:28
(for x being Element of E holds x in A) implies E = A;
theorem :: SUBSET_1:29
E <> {} implies for B for x being Element of E st not x in B holds x in B`;
theorem :: SUBSET_1:30
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:31
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:32
for A,B st for x being Element of E holds not(x in A iff x in B) holds A = B`
;
reserve x1,x2,x3,x4,x5,x6,x7,x8 for Element of X;
theorem :: SUBSET_1:33
X <> {} implies {x1} is Subset of X;
theorem :: SUBSET_1:34
X <> {} implies {x1,x2} is Subset of X;
theorem :: SUBSET_1:35
X <> {} implies {x1,x2,x3} is Subset of X;
theorem :: SUBSET_1:36
X <> {} implies {x1,x2,x3,x4} is Subset of X;
theorem :: SUBSET_1:37
X <> {} implies {x1,x2,x3,x4,x5} is Subset of X;
theorem :: SUBSET_1:38
X <> {} implies {x1,x2,x3,x4,x5,x6} is Subset of X;
theorem :: SUBSET_1:39
X <> {} implies {x1,x2,x3,x4,x5,x6,x7} is Subset of X;
theorem :: SUBSET_1:40
X <> {} implies {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of X;
theorem :: SUBSET_1:41
x in X implies {x} is Subset of X;
scheme :: SUBSET_1:sch 1
SubsetEx { A()-> set, P[object] } :
ex X being Subset of A() st for x holds x
in X iff x in A() & P[x];
scheme :: SUBSET_1:sch 2
SubsetEq {X() -> set, X1,X2()-> Subset of X(), P[set]}: X1() = X2()
provided
for y being Element of X() holds y in X1() iff P[y] and
for y being Element of X() holds y in X2() iff P[y];
definition
let X, Y be non empty set;
redefine pred X misses Y;
irreflexivity;
end;
definition
let X, Y be non empty set;
redefine pred X meets Y;
reflexivity;
end;
definition
::$CD
end;
begin
:: from SETWISEO, 2005.6.11 , A.T.
scheme :: SUBSET_1:sch 3
SubsetEx { A() -> non empty set, P[object] } :
ex B being Subset of A() st for
x being Element of A() holds x in B iff P[x];
:: from GROUP_2, 2005.6.14 , A.T.
scheme :: SUBSET_1:sch 4
SubComp{A() -> set, F1,F2() -> Subset of A(), P[set]}: F1() = F2()
provided
for X being Element of A() holds X in F1() iff P[X] and
for X being Element of A() holds X in F2() iff P[X];
:: from FIN_TOPO, 2006.11.07. A.T.
theorem :: SUBSET_1:42
A` = B` implies A = B;
:: from SGRAPH1, 2008.06.02
registration
let X be empty set;
cluster -> empty for Subset of X;
end;
:: from TEX_2, 2006.06.18, A.T. (simplified)
definition
let E be set;
let A be Subset of E;
attr A is proper means
:: SUBSET_1:def 6
A <> E;
end;
registration
let E be set;
cluster [#]E -> non proper;
end;
registration
let E be set;
cluster non proper for Subset of E;
end;
registration
let E be non empty set;
cluster non proper -> non empty for Subset of E;
cluster empty -> proper for Subset of E;
end;
registration
let E be non empty set;
cluster proper for Subset of E;
end;
registration
let E be empty set;
cluster -> non proper for Subset of E;
end;
:: from GRCAT_1, 2010.02.18, A.T.
theorem :: SUBSET_1:43
for X,Y,A being set, z being set st z in A & A c= [:X,Y:] ex x
being Element of X, y being Element of Y st z = [x,y];
:: from BORSUK_4, 2011.03.04, A.T.
theorem :: SUBSET_1:44
for X being non empty set, A, B being non empty Subset of X st A c< B
ex p being Element of X st p in B & A c= B \ {p};
definition
let X be set;
redefine attr X is trivial means
:: SUBSET_1:def 7
for x,y being Element of X holds x = y;
end;
registration let X be non empty set;
cluster non empty trivial for Subset of X;
end;
registration
let X be trivial set;
cluster -> trivial for Subset of X;
end;
registration
let X be non trivial set;
cluster non trivial for Subset of X;
end;
theorem :: SUBSET_1:45
for D being set, A being Subset of D st A is non trivial
ex d1,d2 being Element of D st d1 in A & d2 in A & d1 <> d2;
theorem :: SUBSET_1:46
for X being trivial non empty set
ex x being Element of X st X = {x};
:: from BORSUK_4, 2011.07.31, A.T.
theorem :: SUBSET_1:47
for X being non empty set, A being non empty Subset of X holds A
is trivial implies ex x being Element of X st A = {x};
theorem :: SUBSET_1:48
for X be non trivial set, x being Element of X
ex y be object st y in X & x <> y;
:: from FUNCT_7, 3.20.2012, A.T.
reserve x for object;
definition
let x,X;
assume
x in X;
func In(x,X) -> Element of X equals
:: SUBSET_1:def 8
x;
end;
registration
let X be non empty set, x be Element of X;
reduce In(x,X) to x;
end;
theorem :: SUBSET_1:49
x in X /\ Y implies In(x,X) = In(x,Y);
:: from BORSUK_4, 2012.08.12, A.T.
theorem :: SUBSET_1:50
for X being non trivial set, p being set ex q being Element of X st q <> p;
theorem :: SUBSET_1:51
for T being non trivial set, X being non trivial Subset of T, p
being set ex q being Element of T st q in X & q <> p;
:: 2012.12.16, A.T.
scheme :: SUBSET_1:sch 5
Union1 { A()-> set, a()-> Element of A(), F(object) -> set }:
union { F(j) where j is Element of A() : j in {a()}} = F(a());
scheme :: SUBSET_1:sch 6
Union2 { A()-> set, a,b()-> Element of A(), F(object) -> set }:
union { F(j) where j is Element of A() : j in {a(),b()}} = F(a()) \/ F(b());