Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

### The abstract of the Mizar article:

### Many-sorted Sets

**by****Andrzej Trybulec**- Received July 7, 1993
- MML identifier: PBOOLE

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, MATRIX_1, RELAT_1, CARD_1, BOOLE, ZF_REFLE, AMI_1, FUNCOP_1, CAT_4, LATTICES, CQC_LANG, PBOOLE; notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, CQC_LANG, CARD_1, AMI_1, MATRIX_1; constructors AMI_1, MATRIX_1, FUNCOP_1, MEMBERED, XBOOLE_0; clusters FUNCT_1, RELAT_1, FUNCOP_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements BOOLE, SUBSET; begin reserve i,e,u for set; definition let f be Function; redefine attr f is empty-yielding means :: PBOOLE:def 1 for i st i in dom f holds f.i is empty; end; definition cluster empty-yielding Function; end; theorem :: PBOOLE:1 for f being Function st f is non-empty holds rng f is with_non-empty_elements; theorem :: PBOOLE:2 for f being Function holds f is empty-yielding iff f = {} or rng f = { {} }; reserve I for set; :: of indices definition let I; canceled; mode ManySortedSet of I -> Function means :: PBOOLE:def 3 dom it = I; end; reserve x,X,Y,Z,V for ManySortedSet of I; scheme Kuratowski_Function{A()-> set, F(set) -> set}: ex f being ManySortedSet of A() st for e st e in A() holds f.e in F(e) provided for e st e in A() holds F(e) <> {}; definition let I,X,Y; pred X in Y means :: PBOOLE:def 4 for i st i in I holds X.i in Y.i; pred X c= Y means :: PBOOLE:def 5 for i st i in I holds X.i c= Y.i; reflexivity; end; definition let I be non empty set,X,Y be ManySortedSet of I; redefine pred X in Y; asymmetry; end; scheme PSeparation { I()-> set, A() -> ManySortedSet of I(), P[set,set] } : ex X being ManySortedSet of I() st for i being set st i in I() for e holds e in X.i iff e in A().i & P[i,e]; theorem :: PBOOLE:3 (for i st i in I holds X.i = Y.i) implies X = Y; definition let I; func [0]I -> ManySortedSet of I equals :: PBOOLE:def 6 I --> {}; let X,Y; func X \/ Y -> ManySortedSet of I means :: PBOOLE:def 7 for i st i in I holds it.i = X.i \/ Y.i; commutativity; idempotence; func X /\ Y -> ManySortedSet of I means :: PBOOLE:def 8 for i st i in I holds it.i = X.i /\ Y.i; commutativity; idempotence; func X \ Y -> ManySortedSet of I means :: PBOOLE:def 9 for i st i in I holds it.i = X.i \ Y.i; pred X overlaps Y means :: PBOOLE:def 10 for i st i in I holds X.i meets Y.i; symmetry; antonym X does_not_overlap Y; pred X misses Y means :: PBOOLE:def 11 for i st i in I holds X.i misses Y.i; symmetry; antonym X meets Y; end; definition let I,X,Y; func X \+\ Y -> ManySortedSet of I equals :: PBOOLE:def 12 (X \ Y) \/ (Y \ X); commutativity; end; theorem :: PBOOLE:4 for i st i in I holds (X \+\ Y).i = X.i \+\ Y.i; theorem :: PBOOLE:5 for i st i in I holds [0]I.i = {}; theorem :: PBOOLE:6 (for i st i in I holds X.i = {}) implies X = [0]I; theorem :: PBOOLE:7 x in X or x in Y implies x in X \/ Y; theorem :: PBOOLE:8 x in X /\ Y iff x in X & x in Y; theorem :: PBOOLE:9 x in X & X c= Y implies x in Y; theorem :: PBOOLE:10 x in X & x in Y implies X overlaps Y; theorem :: PBOOLE:11 X overlaps Y implies ex x st x in X & x in Y; theorem :: PBOOLE:12 x in X \ Y implies x in X; begin :: Lattice properties theorem :: PBOOLE:13 X c= X; definition let I,X,Y; redefine pred X = Y means :: PBOOLE:def 13 X c= Y & Y c= X; end; canceled; theorem :: PBOOLE:15 X c= Y & Y c= Z implies X c= Z; theorem :: PBOOLE:16 X c= X \/ Y & Y c= X \/ Y; theorem :: PBOOLE:17 X /\ Y c= X & X /\ Y c= Y; theorem :: PBOOLE:18 X c= Z & Y c= Z implies X \/ Y c= Z; theorem :: PBOOLE:19 Z c= X & Z c= Y implies Z c= X /\ Y; theorem :: PBOOLE:20 X c= Y implies X \/ Z c= Y \/ Z & Z \/ X c= Z \/ Y; theorem :: PBOOLE:21 X c= Y implies X /\ Z c= Y /\ Z & Z /\ X c= Z /\ Y; theorem :: PBOOLE:22 X c= Y & Z c= V implies X \/ Z c= Y \/ V; theorem :: PBOOLE:23 X c= Y & Z c= V implies X /\ Z c= Y /\ V; theorem :: PBOOLE:24 X c= Y implies X \/ Y = Y & Y \/ X = Y; theorem :: PBOOLE:25 X c= Y implies X /\ Y = X & Y /\ X = X; theorem :: PBOOLE:26 X /\ Y c= X \/ Z; theorem :: PBOOLE:27 X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z; theorem :: PBOOLE:28 X = Y \/ Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V; theorem :: PBOOLE:29 X = Y /\ Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X; canceled 4; theorem :: PBOOLE:34 (X \/ Y) \/ Z = X \/ (Y \/ Z); theorem :: PBOOLE:35 (X /\ Y) /\ Z = X /\ (Y /\ Z); theorem :: PBOOLE:36 X /\ (X \/ Y) = X & (X \/ Y) /\ X = X & X /\ (Y \/ X) = X & (Y \/ X) /\ X = X; theorem :: PBOOLE:37 X \/ (X /\ Y) = X & (X /\ Y) \/ X = X & X \/ (Y /\ X) = X & (Y /\ X) \/ X = X; theorem :: PBOOLE:38 X /\ (Y \/ Z) = X /\ Y \/ X /\ Z; theorem :: PBOOLE:39 X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z) & Y /\ Z \/ X = (Y \/ X) /\ (Z \/ X); theorem :: PBOOLE:40 (X /\ Y) \/ (X /\ Z) = X implies X c= Y \/ Z; theorem :: PBOOLE:41 (X \/ Y) /\ (X \/ Z) = X implies Y /\ Z c= X; theorem :: PBOOLE:42 (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X); theorem :: PBOOLE:43 :: SETWISEO:7 X \/ Y c= Z implies X c= Z & Y c= Z; theorem :: PBOOLE:44 :: SYSREL:4 X c= Y /\ Z implies X c= Y & X c= Z; theorem :: PBOOLE:45 :: SYSREL:2 X \/ Y \/ Z = (X \/ Z) \/ (Y \/ Z) & X \/ (Y \/ Z) = (X \/ Y) \/ (X \/ Z); theorem :: PBOOLE:46 X /\ Y /\ Z = (X /\ Z) /\ (Y /\ Z) & X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z); theorem :: PBOOLE:47 :: SYSREL:3 X \/ (X \/ Y) = X \/ Y & X \/ Y \/ Y = X \/ Y; theorem :: PBOOLE:48 X /\ (X /\ Y) = X /\ Y & X /\ Y /\ Y = X /\ Y; begin :: ManySortedSet with empty components theorem :: PBOOLE:49 [0]I c= X; theorem :: PBOOLE:50 X c= [0]I implies X = [0]I; theorem :: PBOOLE:51 X c= Y & X c= Z & Y /\ Z = [0]I implies X = [0]I; theorem :: PBOOLE:52 X c= Y & Y /\ Z = [0]I implies X /\ Z = [0]I; theorem :: PBOOLE:53 X \/ [0]I = X & [0]I \/ X = X; theorem :: PBOOLE:54 X \/ Y = [0]I implies X = [0]I & Y = [0]I; theorem :: PBOOLE:55 X /\ [0]I = [0]I & [0]I /\ X = [0]I; theorem :: PBOOLE:56 X c= (Y \/ Z) & X /\ Z = [0]I implies X c= Y; theorem :: PBOOLE:57 Y c= X & X /\ Y = [0]I implies Y = [0]I; begin :: Difference and symmetric difference theorem :: PBOOLE:58 X \ Y = [0]I iff X c= Y; theorem :: PBOOLE:59 X c= Y implies X \ Z c= Y \ Z; theorem :: PBOOLE:60 X c= Y implies Z \ Y c= Z \ X; theorem :: PBOOLE:61 X c= Y & Z c= V implies X \ V c= Y \ Z; theorem :: PBOOLE:62 X \ Y c= X; theorem :: PBOOLE:63 X c= Y \ X implies X = [0]I; theorem :: PBOOLE:64 X \ X = [0]I; theorem :: PBOOLE:65 X \ [0]I = X; theorem :: PBOOLE:66 [0]I \ X = [0]I; theorem :: PBOOLE:67 X \ (X \/ Y) = [0]I & X \ (Y \/ X) = [0]I; theorem :: PBOOLE:68 X /\ (Y \ Z) = (X /\ Y) \ Z; theorem :: PBOOLE:69 (X \ Y) /\ Y = [0]I & Y /\ (X \ Y) = [0]I; theorem :: PBOOLE:70 X \ (Y \ Z) = (X \ Y) \/ X /\ Z; theorem :: PBOOLE:71 (X \ Y) \/ X /\ Y = X & X /\ Y \/ (X \ Y) = X; theorem :: PBOOLE:72 X c= Y implies Y = X \/ (Y \ X) & Y = (Y \ X) \/ X; theorem :: PBOOLE:73 X \/ (Y \ X) = X \/ Y & (Y \ X) \/ X = Y \/ X; theorem :: PBOOLE:74 X \ (X \ Y) = X /\ Y; theorem :: PBOOLE:75 X \ (Y /\ Z) = (X \ Y) \/ (X \ Z); theorem :: PBOOLE:76 X \ X /\ Y = X \ Y & X \ Y /\ X = X \ Y; theorem :: PBOOLE:77 X /\ Y = [0]I iff X \ Y = X; theorem :: PBOOLE:78 (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z); theorem :: PBOOLE:79 (X \ Y) \ Z = X \ (Y \/ Z); theorem :: PBOOLE:80 :: TSEP_1, LEMMA3 (X /\ Y) \ Z = (X \ Z) /\ (Y \ Z); theorem :: PBOOLE:81 (X \/ Y) \ Y = X \ Y; theorem :: PBOOLE:82 X c= Y \/ Z implies X \ Y c= Z & X \ Z c= Y; theorem :: PBOOLE:83 (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X); theorem :: PBOOLE:84 (X \ Y) \ Y = X \ Y; theorem :: PBOOLE:85 X \ (Y \/ Z) = (X \ Y) /\ (X \ Z); theorem :: PBOOLE:86 X \ Y = Y \ X implies X = Y; theorem :: PBOOLE:87 X /\ (Y \ Z) = X /\ Y \ X /\ Z; theorem :: PBOOLE:88 :: NORMFORM:2 X \ Y c= Z implies X c= Y \/ Z; theorem :: PBOOLE:89 X \ Y c= X \+\ Y; canceled; theorem :: PBOOLE:91 X \+\ [0]I = X & [0]I \+\ X = X; theorem :: PBOOLE:92 X \+\ X = [0]I; canceled; theorem :: PBOOLE:94 X \/ Y = (X \+\ Y) \/ X /\ Y; theorem :: PBOOLE:95 X \+\ Y = (X \/ Y) \ X /\ Y; theorem :: PBOOLE:96 (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z)); theorem :: PBOOLE:97 X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z; theorem :: PBOOLE:98 (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z); theorem :: PBOOLE:99 X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z; theorem :: PBOOLE:100 :: FINSUB_1:3 X \/ Y = X \+\ (Y \ X); theorem :: PBOOLE:101 X /\ Y = X \+\ (X \ Y); theorem :: PBOOLE:102 :: FINSUB_1:5 X \ Y = X \+\ (X /\ Y); theorem :: PBOOLE:103 Y \ X = X \+\ (X \/ Y); theorem :: PBOOLE:104 :: FINSUB_1:4 X \/ Y = X \+\ Y \+\ X /\ Y; theorem :: PBOOLE:105 :: FINSUB_1:6 X /\ Y = X \+\ Y \+\ (X \/ Y); begin :: Meeting and overlap(p?)ing theorem :: PBOOLE:106 X overlaps Y or X overlaps Z implies X overlaps Y \/ Z; canceled; theorem :: PBOOLE:108 X overlaps Y & Y c= Z implies X overlaps Z; theorem :: PBOOLE:109 X overlaps Y & X c= Z implies Z overlaps Y; theorem :: PBOOLE:110 :: NORMFORM:1 X c= Y & Z c= V & X overlaps Z implies Y overlaps V; theorem :: PBOOLE:111 X overlaps Y /\ Z implies X overlaps Y & X overlaps Z; theorem :: PBOOLE:112 :: BORSUK_1:1 X overlaps Z & X c= V implies X overlaps Z /\ V; theorem :: PBOOLE:113 X overlaps Y \ Z implies X overlaps Y; theorem :: PBOOLE:114 :: PROB_2:7, RPR_1:36 Y does_not_overlap Z implies X /\ Y does_not_overlap X /\ Z; theorem :: PBOOLE:115 :: AMI_2:1 X overlaps Y \ Z implies Y overlaps X \ Z; theorem :: PBOOLE:116 X meets Y & Y c= Z implies X meets Z; canceled; theorem :: PBOOLE:118 Y misses X \ Y; theorem :: PBOOLE:119 X /\ Y misses X \ Y; theorem :: PBOOLE:120 X /\ Y misses X \+\ Y; theorem :: PBOOLE:121 X misses Y implies X /\ Y = [0]I; theorem :: PBOOLE:122 X <> [0]I implies X meets X; theorem :: PBOOLE:123 X c= Y & X c= Z & Y misses Z implies X = [0]I; theorem :: PBOOLE:124 :: SETWISEO:9 Z \/ V = X \/ Y & X misses Z & Y misses V implies X = V & Y = Z; canceled; theorem :: PBOOLE:126 :: FINSUB_1:1 X misses Y implies X \ Y = X; theorem :: PBOOLE:127 :: FINSUB_1:2 X misses Y implies (X \/ Y) \ Y = X; theorem :: PBOOLE:128 :: RPR_1:32 X \ Y = X implies X misses Y; theorem :: PBOOLE:129 :: RLVECT_2:102 X \ Y misses Y \ X; begin :: Roughly speaking definition let I,X,Y; pred X [= Y means :: PBOOLE:def 14 for x st x in X holds x in Y; reflexivity; end; theorem :: PBOOLE:130 X c= Y implies X [= Y; theorem :: PBOOLE:131 X [= X; theorem :: PBOOLE:132 X [= Y & Y [= Z implies X [= Z; begin :: Non empty set of sorts theorem :: PBOOLE:133 [0]{} in [0]{}; theorem :: PBOOLE:134 for X being ManySortedSet of {} holds X = {}; reserve I for non empty set, x,X,Y for ManySortedSet of I; theorem :: PBOOLE:135 X overlaps Y implies X meets Y; theorem :: PBOOLE:136 not ex x st x in [0]I; theorem :: PBOOLE:137 x in X & x in Y implies X /\ Y <> [0]I; theorem :: PBOOLE:138 X does_not_overlap [0]I & [0]I does_not_overlap X; theorem :: PBOOLE:139 X /\ Y = [0]I implies X does_not_overlap Y; theorem :: PBOOLE:140 X overlaps X implies X <> [0]I; begin :: Empty and non-empty ManySortedSets reserve I for set, x,X,Y,Z for ManySortedSet of I; definition let I be set; let X be ManySortedSet of I; redefine attr X is empty-yielding means :: PBOOLE:def 15 for i st i in I holds X.i is empty; attr X is non-empty means :: PBOOLE:def 16 for i st i in I holds X.i is non empty; end; definition let I be set; cluster empty-yielding ManySortedSet of I; cluster non-empty ManySortedSet of I; end; definition let I be non empty set; cluster non-empty -> non empty-yielding ManySortedSet of I; cluster empty-yielding -> non non-empty ManySortedSet of I; end; theorem :: PBOOLE:141 X is empty-yielding iff X = [0]I; theorem :: PBOOLE:142 Y is empty-yielding & X c= Y implies X is empty-yielding; theorem :: PBOOLE:143 X is non-empty & X c= Y implies Y is non-empty; theorem :: PBOOLE:144 X is non-empty & X [= Y implies X c= Y; theorem :: PBOOLE:145 X is non-empty & X [= Y implies Y is non-empty; reserve X for non-empty ManySortedSet of I; theorem :: PBOOLE:146 ex x st x in X; theorem :: PBOOLE:147 (for x holds x in X iff x in Y) implies X = Y; theorem :: PBOOLE:148 (for x holds x in X iff x in Y & x in Z) implies X = Y /\ Z;

Back to top