Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Boolean Properties of Sets

**by****Zinaida Trybulec, and****Halina Swieczkowska**- Received January 6, 1989
- MML identifier: BOOLE

- [ Mizar article, MML identifier index ]

environ vocabulary TARSKI, BOOLE; notation TARSKI; constructors TARSKI; begin reserve x,y,z for set, X,Y,Z,V for set; scheme Separation { A()-> set, P[set] } : ex X st for x holds x in X iff x in A() & P[x]; definition func {} -> set means :: BOOLE:def 1 not ex x st x in it; let X,Y; func X \/ Y -> set means :: BOOLE:def 2 x in it iff x in X or x in Y; commutativity; idempotence; func X /\ Y -> set means :: BOOLE:def 3 x in it iff x in X & x in Y; commutativity; idempotence; func X \ Y -> set means :: BOOLE:def 4 x in it iff x in X & not x in Y; end; definition let X,Y; pred X misses Y means :: BOOLE:def 5 X /\ Y = {}; symmetry; antonym X meets Y; end; definition let X,Y; canceled; func X \+\ Y -> set equals :: BOOLE:def 7 (X \ Y) \/ (Y \ X); commutativity; end; :: :: THEOREMS RELATED TO MEMBERSHIP :: :: 1.Definitional theorems :: definition let X,Y; redefine pred X = Y means :: BOOLE:def 8 X c= Y & Y c= X; end; theorem :: BOOLE:1 X meets Y iff ex x st x in X & x in Y; theorem :: BOOLE:2 X meets Y iff ex x st x in X /\ Y; canceled 20; theorem :: BOOLE:23 x in X \+\ Y iff not (x in X iff x in Y); canceled; theorem :: BOOLE:25 (for x holds not x in X iff (x in Y iff x in Z)) implies X = Y \+\ Z; :: :: THEOREMS IN WHICH "in" DOES NOT OCCUR :: :: 2.1 Theorems related to inclusion :: canceled; theorem :: BOOLE:27 {} c= X; canceled; theorem :: BOOLE:29 X c= Y & Y c= Z implies X c= Z; theorem :: BOOLE:30 X c= {} implies X = {}; theorem :: BOOLE:31 X c= X \/ Y; theorem :: BOOLE:32 X c= Z & Y c= Z implies X \/ Y c= Z; theorem :: BOOLE:33 X c= Y implies X \/ Z c= Y \/ Z; theorem :: BOOLE:34 X c= Y & Z c= V implies X \/ Z c= Y \/ V; theorem :: BOOLE:35 X c= Y implies X \/ Y = Y; canceled; theorem :: BOOLE:37 X /\ Y c= X; theorem :: BOOLE:38 X /\ Y c= X \/ Z; theorem :: BOOLE:39 Z c= X & Z c= Y implies Z c= X /\ Y; theorem :: BOOLE:40 X c= Y implies X /\ Z c= Y /\ Z; theorem :: BOOLE:41 X c= Y & Z c= V implies X /\ Z c= Y /\ V; theorem :: BOOLE:42 X c= Y implies X /\ Y = X; canceled; theorem :: BOOLE:44 X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z; theorem :: BOOLE:45 X \ Y = {} iff X c= Y; theorem :: BOOLE:46 X c= Y implies X \ Z c= Y \ Z; theorem :: BOOLE:47 X c= Y implies Z \ Y c= Z \ X; theorem :: BOOLE:48 X c= Y & Z c= V implies X \ V c= Y \ Z; theorem :: BOOLE:49 X \ Y c= X; theorem :: BOOLE:50 X c= Y \ X implies X = {}; theorem :: BOOLE:51 X c= Y & X c= Z & Y misses Z implies X = {}; theorem :: BOOLE:52 X c= Y \/ Z implies X \ Y c= Z; theorem :: BOOLE:53 (X /\ Y) \/ (X /\ Z) = X implies X c= Y \/ Z; theorem :: BOOLE:54 X c= Y implies Y = X \/ (Y \ X); theorem :: BOOLE:55 X c= Y & Y misses Z implies X misses Z; theorem :: BOOLE:56 X = Y \/ Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V; theorem :: BOOLE:57 X = Y /\ Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X; theorem :: BOOLE:58 X \ Y c= X \+\ Y; :: :: 2.2 Identities :: theorem :: BOOLE:59 X \/ Y = {} implies X = {} & Y = {}; theorem :: BOOLE:60 X \/ {} = X; theorem :: BOOLE:61 X misses {}; canceled 2; theorem :: BOOLE:64 (X \/ Y) \/ Z = X \/ (Y \/ Z); canceled 2; theorem :: BOOLE:67 (X /\ Y) /\ Z = X /\ (Y /\ Z); theorem :: BOOLE:68 X /\ (X \/ Y) = X; theorem :: BOOLE:69 X \/ (X /\ Y) = X; theorem :: BOOLE:70 X /\ (Y \/ Z) = X /\ Y \/ X /\ Z; theorem :: BOOLE:71 X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z); theorem :: BOOLE:72 (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X); canceled; theorem :: BOOLE:74 X \ {} = X; theorem :: BOOLE:75 {} \ X = {}; theorem :: BOOLE:76 X \ (X \/ Y) = {}; theorem :: BOOLE:77 X \ X /\ Y = X \ Y; theorem :: BOOLE:78 X \ Y misses Y; theorem :: BOOLE:79 X \/ (Y \ X) = X \/ Y; theorem :: BOOLE:80 X /\ Y \/ (X \ Y) = X; theorem :: BOOLE:81 X \ (Y \ Z) = (X \ Y) \/ X /\ Z; theorem :: BOOLE:82 X \ (X \ Y) = X /\ Y; theorem :: BOOLE:83 (X \/ Y) \ Y = X \ Y; theorem :: BOOLE:84 X misses Y iff X \ Y = X; theorem :: BOOLE:85 X \ (Y \/ Z) = (X \ Y) /\ (X \ Z); theorem :: BOOLE:86 X \ (Y /\ Z) = (X \ Y) \/ (X \ Z); theorem :: BOOLE:87 (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X); theorem :: BOOLE:88 (X \ Y) \ Z = X \ (Y \/ Z); theorem :: BOOLE:89 (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z); theorem :: BOOLE:90 X \ Y = Y \ X implies X = Y; canceled; theorem :: BOOLE:92 X \+\ {} = X; theorem :: BOOLE:93 X \+\ X = {}; canceled; theorem :: BOOLE:95 X \/ Y = (X \+\ Y) \/ X /\ Y; theorem :: BOOLE:96 X \+\ Y = (X \/ Y) \ X /\ Y; theorem :: BOOLE:97 (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z)); theorem :: BOOLE:98 X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z; theorem :: BOOLE:99 (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z); :: :: 2.3 "meets" and "misses" :: theorem :: BOOLE:100 X meets Y \/ Z iff X meets Y or X meets Z; theorem :: BOOLE:101 X meets Y & Y c= Z implies X meets Z; theorem :: BOOLE:102 X meets Y /\ Z implies X meets Y; canceled; theorem :: BOOLE:104 X misses {}; canceled 5; theorem :: BOOLE:110 X meets X iff X <> {}; theorem :: BOOLE:111 X /\ Y misses X \ Y; theorem :: BOOLE:112 X /\ Y misses X \+\ Y; theorem :: BOOLE:113 X meets Y \ Z implies X meets Y; theorem :: BOOLE:114 X c= Y & X c= Z & Y misses Z implies X = {}; :: :: ADDITIONAL THEOREMS :: theorem :: BOOLE:115 X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z; theorem :: BOOLE:116 X /\ (Y \ Z) = (X /\ Y) \ Z; theorem :: BOOLE:117 X /\ (Y \ Z) = X /\ Y \ X /\ Z; canceled 2; theorem :: BOOLE:120 X c= Y \/ Z & X misses Z implies X c= Y; begin :: Addendum, 2000.01.10, A.T. definition let X,Y; pred X c< Y means :: BOOLE:def 9 X c= Y & X <> Y; irreflexivity; end; theorem :: BOOLE:121 X c< Y & Y c= Z implies X c< Z; theorem :: BOOLE:122 X c= Y & Y c< Z implies X c< Z; theorem :: BOOLE:123 X c< Y & Y c< Z implies X c< Z; theorem :: BOOLE:124 X <> {} implies {} c< X; theorem :: BOOLE:125 not ex X st X c< {}; theorem :: BOOLE:126 not ex X,Y st X c< Y & Y c< X; theorem :: BOOLE:127 X c= Y implies not Y c< X;

Back to top