EMM, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Boolean Properties of Sets --- Definitions

**by****Library Committee**- Received April 6, 2002
- MML identifier: XBOOLE_0

- [ Mizar article, MML identifier index ]

environ vocabulary TARSKI, BOOLE, ZFMISC_1; notation TARSKI; constructors TARSKI; begin reserve X, Y, Z, x, y, z for set; scheme Separation { A()-> set, P[set] } : ex X being set st for x being set holds x in X iff x in A() & P[x]; definition func {} -> set means :: XBOOLE_0:def 1 not ex x being set st x in it; let X,Y be set; func X \/ Y -> set means :: XBOOLE_0:def 2 x in it iff x in X or x in Y; commutativity; idempotence; func X /\ Y -> set means :: XBOOLE_0:def 3 x in it iff x in X & x in Y; commutativity; idempotence; func X \ Y -> set means :: XBOOLE_0:def 4 x in it iff x in X & not x in Y; end; definition let X be set; attr X is empty means :: XBOOLE_0:def 5 X = {}; let Y be set; func X \+\ Y -> set equals :: XBOOLE_0:def 6 (X \ Y) \/ (Y \ X); commutativity; pred X misses Y means :: XBOOLE_0:def 7 X /\ Y = {}; symmetry; antonym X meets Y; pred X c< Y means :: XBOOLE_0:def 8 X c= Y & X <> Y; irreflexivity; pred X,Y are_c=-comparable means :: XBOOLE_0:def 9 X c= Y or Y c= X; reflexivity; symmetry; redefine pred X = Y means :: XBOOLE_0:def 10 X c= Y & Y c= X; end; theorem :: XBOOLE_0:1 x in X \+\ Y iff not (x in X iff x in Y); theorem :: XBOOLE_0:2 :: BOOLE'25: (for x holds not x in X iff (x in Y iff x in Z)) implies X = Y \+\ Z; definition cluster {} -> empty; cluster empty set; cluster non empty set; end; definition let D be non empty set, X be set; cluster D \/ X -> non empty; cluster X \/ D -> non empty; end; theorem :: XBOOLE_0:3 :: BOOLE'1: X meets Y iff ex x st x in X & x in Y; theorem :: XBOOLE_0:4 :: BOOLE'2: X meets Y iff ex x st x in X /\ Y; theorem :: XBOOLE_0:5 :: SYSREL'1: X misses Y & x in X \/ Y implies ((x in X & not x in Y) or (x in Y & not x in X)); scheme Extensionality { X,Y() -> set, P[set] } : X() = Y() provided for x holds x in X() iff P[x] and for x holds x in Y() iff P[x]; scheme SetEq { P[set] } : for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for x being set holds x in X2 iff P[x]) holds X1 = X2;

Back to top