:: Boolean Properties of Sets - Definitions
:: by Library Committee
::
:: Received April 6, 2002
:: Copyright (c) 2002-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 TARSKI, XBOOLE_0, MATROID0, AOFA_000;
notations TARSKI;
constructors TARSKI;
definitions TARSKI;
expansions TARSKI;
theorems TARSKI;
schemes TARSKI;
begin
reserve X, Y, Z for set, x, y, z for object;
scheme
Separation { A()-> set, P[object] } :
ex X being set st for x holds x in X iff x in A() & P[x]
proof
defpred Q[object,object] means $1 = $2 & P[$2];
A1: for x,y,z being object st Q[x,y] & Q[x,z] holds y = z;
consider X such that
A2: for x holds x in X iff ex y st y in A() & Q[y,x] from TARSKI:sch 1(A1);
take X;
let x;
thus x in X implies x in A() & P[x]
proof assume x in X;
then ex y st y in A() & Q[y,x] by A2;
hence thesis;
end;
assume x in A() & P[x];
then ex y st y in A() & Q[y,x];
hence x in X by A2;
end;
definition
let X be set;
attr X is empty means
:Def1:
not ex x st x in X;
end;
registration
cluster empty for set;
existence
proof
defpred P[object] means contradiction;
consider Y such that
A1: for x holds x in Y iff x in the set & P[x] from Separation;
take Y;
thus not ex x st x in Y by A1;
end;
end;
definition
func {} -> set equals the empty set;
coherence;
let X,Y be set;
func X \/ Y -> set means
:Def3:
for x holds x in it iff x in X or x in Y;
existence
proof
take union {X,Y};
let x;
thus x in union {X,Y} implies x in X or x in Y
proof
assume x in union {X,Y};
then ex Z being set st x in Z & Z in {X,Y} by TARSKI:def 4;
hence thesis by TARSKI:def 2;
end;
X in {X,Y} & Y in {X,Y} by TARSKI:def 2;
hence thesis by TARSKI:def 4;
end;
uniqueness
proof
let A1, A2 be set such that
A1: for x holds x in A1 iff x in X or x in Y and
A2: for x holds x in A2 iff x in X or x in Y;
now
let x;
x in A1 iff x in X or x in Y by A1;
hence x in A1 iff x in A2 by A2;
end;
hence thesis by TARSKI:2;
end;
commutativity;
idempotence;
func X /\ Y -> set means
:Def4:
for x holds x in it iff x in X & x in Y;
existence
proof
defpred P[object] means $1 in Y;
thus ex Z being set st for x holds x in Z iff x in X & P[x] from
Separation;
end;
uniqueness
proof
let A1, A2 be set such that
A3: for x holds x in A1 iff x in X & x in Y and
A4: for x holds x in A2 iff x in X & x in Y;
now
let x;
x in A1 iff x in X & x in Y by A3;
hence x in A1 iff x in A2 by A4;
end;
hence thesis by TARSKI:2;
end;
commutativity;
idempotence;
func X \ Y -> set means
:Def5:
for x holds x in it iff x in X & not x in Y;
existence
proof
defpred P[object] means not $1 in Y;
thus ex Z being set st
for x holds x in Z iff x in X & P[x] from Separation;
end;
uniqueness
proof
let A1, A2 be set such that
A5: for x holds x in A1 iff x in X & not x in Y and
A6: for x holds x in A2 iff x in X & not x in Y;
now
let x;
x in A1 iff x in X & not x in Y by A5;
hence x in A1 iff x in A2 by A6;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let X, Y be set;
func X \+\ Y -> set equals
(X \ Y) \/ (Y \ X);
correctness;
commutativity;
pred X misses Y means
X /\ Y = {};
symmetry;
pred X c< Y means
:Def8:
X c= Y & X <> Y;
irreflexivity;
asymmetry
by TARSKI:2;
pred X,Y are_c=-comparable means
X c= Y or Y c= X;
reflexivity;
symmetry;
redefine pred X = Y means :: redefines = (HIDDEN, definition)
X c= Y & Y c= X;
compatibility
by TARSKI:2;
end;
notation
let X, Y be set;
antonym X meets Y for X misses Y;
end;
theorem
x in X \+\ Y iff not (x in X iff x in Y)
proof
x in X \+\ Y iff x in X \ Y or x in Y \ X by Def3;
hence thesis by Def5;
end;
theorem
(for x holds not x in X iff (x in Y iff x in Z)) implies X = Y \+\ Z
proof
assume
A1: not x in X iff (x in Y iff x in Z);
now
let x;
x in X iff x in Y & not x in Z or x in Z & not x in Y by A1;
then x in X iff x in Y \ Z or x in Z \ Y by Def5;
hence x in X iff x in Y \+\ Z by Def3;
end;
hence thesis by TARSKI:2;
end;
registration
cluster {} -> empty;
coherence;
end;
registration
let x;
cluster { x } -> non empty;
coherence
proof
x in {x} by TARSKI:def 1;
hence ex z st z in {x};
end;
let y;
cluster { x, y } -> non empty;
coherence
proof
x in {x,y} by TARSKI:def 2;
hence ex z st z in {x,y};
end;
end;
registration
cluster non empty for set;
existence
proof
take { the set };
thus thesis;
end;
end;
registration
let D be non empty set, X be set;
cluster D \/ X -> non empty;
coherence
proof
consider x such that
A1: x in D by Def1;
x in D \/ X by A1,Def3;
hence ex x st x in D \/ X;
end;
cluster X \/ D -> non empty;
coherence;
end;
Lm1: X is empty implies X = {}
proof
assume not ex x st x in X;
then for x holds x in {} iff x in X by Def1;
hence thesis by TARSKI:2;
end;
theorem Th3:
X meets Y iff ex x st x in X & x in Y
proof
hereby
assume X meets Y;
then X /\ Y <> {};
then X /\ Y is not empty by Lm1;
then consider x such that
A1: x in X /\ Y;
take x;
thus x in X & x in Y by A1,Def4;
end;
given x such that
A2: x in X & x in Y;
x in X /\ Y by A2,Def4;
then X /\ Y <> {} by Def1;
hence thesis;
end;
theorem
X meets Y iff ex x st x in X /\ Y
proof
hereby
assume X meets Y;
then X /\ Y <> {};
then X /\ Y is not empty by Lm1;
then consider x such that
A1: x in X /\ Y;
take x;
thus x in X /\ Y by A1;
end;
assume ex x st x in X /\ Y;
then X /\ Y <> {} by Def1;
hence thesis;
end;
theorem
X misses Y & x in X \/ Y implies x in X & not x in Y or x in Y & not x in X
by Def3,Th3;
scheme
Extensionality { X,Y() -> set, P[object] } :
X() = Y()
provided
A1: for x holds x in X() iff P[x] and
A2: for x holds x in Y() iff P[x]
proof
A3: for x holds x in Y() implies x in X()
by A1,A2;
for x holds x in X() implies x in Y()
by A1,A2;
hence thesis by A3,TARSKI:2;
end;
scheme
SetEq { P[object] } :
for X1,X2 being set st
(for x holds x in X1 iff P[x]) &
(for x holds x in X2 iff P[x]) holds X1 = X2
proof
let X1,X2 be set such that
A1: for x holds x in X1 iff P[x] and
A2: for x holds x in X2 iff P[x];
thus thesis from Extensionality(A1,A2);
end;
begin :: Addenda
:: from RLSUB_2, 2006.12.02, AT
theorem Th6:
X c< Y implies ex x st x in Y & not x in X
by Def8,TARSKI:def 3;
:: 2008.08.07, A.T.
theorem
X <> {} implies ex x st x in X
by Def1,Lm1;
:: 2012.10.08, A.T.
theorem
X c< Y implies ex x st x in Y & X c= Y \ {x}
proof
assume
A1: X c< Y;
then consider x such that
A2: x in Y and
A3: not x in X by Th6;
take x;
thus x in Y by A2;
let y;
assume
A4: y in X;
then y <> x by A3;
then
A5: not y in {x} by TARSKI:def 1;
X c= Y by A1;
then y in Y by A4;
hence thesis by Def5,A5;
end;
:: from MATROID0, 2013.01.18, A.T.
notation
let x,y be set;
antonym x c/= y for x c= y;
end;
:: from AOFA_000, 2013.01.18, A.T.
notation
let x be object,y be set;
antonym x nin y for x in y;
end;