:: Manysorted Sets :: by Andrzej Trybulec :: :: Received July 7, 1993 :: Copyright (c) 1993-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 FUNCT_1, RELAT_1, SETFAM_1, XBOOLE_0, SUBSET_1, PARTFUN1, FUNCOP_1, TARSKI, FUNCT_2, ZFMISC_1, MEMBER_1, FUNCT_4, PBOOLE, NAT_1, SETLIM_2; notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1; constructors SETFAM_1, FUNCOP_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_4; registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FUNCT_4, RELAT_1; requirements BOOLE, SUBSET; begin reserve i,j,e,u for object; 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 registration let I; cluster total for I-defined Function; end; definition let I; mode ManySortedSet of I is total I-defined Function; end; reserve x,X,Y,Z,V for ManySortedSet of I; scheme :: PBOOLE:sch 1 KuratowskiFunction{A()-> set, F(object) -> set}: ex f being ManySortedSet of A() st for e being object st e in A() holds f.e in F(e) provided for e being object st e in A() holds F(e) <> {}; definition let I,X,Y; pred X in Y means :: PBOOLE:def 1 for i being object st i in I holds X.i in Y.i; pred X c= Y means :: PBOOLE:def 2 for i being object 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 :: PBOOLE:sch 2 PSeparation { I()-> set, A() -> ManySortedSet of I(), P[object,object] } : ex X being ManySortedSet of I() st for i being object st i in I() for e being object holds e in X.i iff e in A().i & P[i,e]; theorem :: PBOOLE:3 (for i being object st i in I holds X.i = Y.i) implies X = Y; definition let I; func EmptyMS I -> ManySortedSet of I equals :: PBOOLE:def 3 I --> {}; let X,Y; func X (\/) Y -> ManySortedSet of I means :: PBOOLE:def 4 for i being object st i in I holds it.i = X.i \/ Y.i; commutativity; idempotence; func X (/\) Y -> ManySortedSet of I means :: PBOOLE:def 5 for i being object st i in I holds it.i = X.i /\ Y.i; commutativity; idempotence; func X (\) Y -> ManySortedSet of I means :: PBOOLE:def 6 for i being object st i in I holds it.i = X.i \ Y.i; pred X overlaps Y means :: PBOOLE:def 7 for i being object st i in I holds X.i meets Y.i; symmetry; pred X misses Y means :: PBOOLE:def 8 for i being object st i in I holds X.i misses Y.i; symmetry; end; notation let I; let X,Y; antonym X meets Y for X misses Y; end; definition let I,X,Y; func X (\+\) Y -> ManySortedSet of I equals :: PBOOLE:def 9 (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 being object holds EmptyMS I.i = {}; theorem :: PBOOLE:6 (for i being object st i in I holds X.i = {}) implies X = EmptyMS 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 definition let I,X,Y; redefine pred X = Y means :: PBOOLE:def 10 for i being object st i in I holds X.i = Y.i; end; theorem :: PBOOLE:13 X c= Y & Y c= Z implies X c= Z; theorem :: PBOOLE:14 X c= X (\/) Y; theorem :: PBOOLE:15 X (/\) Y c= X; theorem :: PBOOLE:16 X c= Z & Y c= Z implies X (\/) Y c= Z; theorem :: PBOOLE:17 Z c= X & Z c= Y implies Z c= X (/\) Y; theorem :: PBOOLE:18 X c= Y implies X (\/) Z c= Y (\/) Z; theorem :: PBOOLE:19 X c= Y implies X (/\) Z c= Y (/\) Z; theorem :: PBOOLE:20 X c= Y & Z c= V implies X (\/) Z c= Y (\/) V; theorem :: PBOOLE:21 X c= Y & Z c= V implies X (/\) Z c= Y (/\) V; theorem :: PBOOLE:22 X c= Y implies X (\/) Y = Y; theorem :: PBOOLE:23 X c= Y implies X (/\) Y = X; theorem :: PBOOLE:24 X (/\) Y c= X (\/) Z; theorem :: PBOOLE:25 X c= Z implies X (\/) Y (/\) Z = (X (\/) Y) (/\) Z; theorem :: PBOOLE:26 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:27 X = Y (/\) Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X; theorem :: PBOOLE:28 (X (\/) Y) (\/) Z = X (\/) (Y (\/) Z); theorem :: PBOOLE:29 (X (/\) Y) (/\) Z = X (/\) (Y (/\) Z); theorem :: PBOOLE:30 X (/\) (X (\/) Y) = X; theorem :: PBOOLE:31 X (\/) (X (/\) Y) = X; theorem :: PBOOLE:32 X (/\) (Y (\/) Z) = X (/\) Y (\/) X (/\) Z; theorem :: PBOOLE:33 X (\/) Y (/\) Z = (X (\/) Y) (/\) (X (\/) Z); theorem :: PBOOLE:34 (X (/\) Y) (\/) (X (/\) Z) = X implies X c= Y (\/) Z; theorem :: PBOOLE:35 (X (\/) Y) (/\) (X (\/) Z) = X implies Y (/\) Z c= X; theorem :: PBOOLE:36 (X (/\) Y) (\/) (Y (/\) Z) (\/) (Z (/\) X) = (X (\/) Y) (/\) (Y (\/) Z) (/\) (Z (\/) X); theorem :: PBOOLE:37 X (\/) Y c= Z implies X c= Z; theorem :: PBOOLE:38 X c= Y (/\) Z implies X c= Y; theorem :: PBOOLE:39 X (\/) Y (\/) Z = (X (\/) Z) (\/) (Y (\/) Z); theorem :: PBOOLE:40 X (/\) Y (/\) Z = (X (/\) Z) (/\) (Y (/\) Z); theorem :: PBOOLE:41 X (\/) (X (\/) Y) = X (\/) Y; theorem :: PBOOLE:42 X (/\) (X (/\) Y) = X (/\) Y; begin :: ManySortedSet with empty components theorem :: PBOOLE:43 EmptyMS I c= X; theorem :: PBOOLE:44 X c= EmptyMS I implies X = EmptyMS I; theorem :: PBOOLE:45 X c= Y & X c= Z & Y (/\) Z = EmptyMS I implies X = EmptyMS I; theorem :: PBOOLE:46 X c= Y & Y (/\) Z = EmptyMS I implies X (/\) Z = EmptyMS I; theorem :: PBOOLE:47 X (\/) EmptyMS I = X & EmptyMS I (\/) X = X; theorem :: PBOOLE:48 X (\/) Y = EmptyMS I implies X = EmptyMS I; theorem :: PBOOLE:49 X (/\) EmptyMS I = EmptyMS I; theorem :: PBOOLE:50 X c= (Y (\/) Z) & X (/\) Z = EmptyMS I implies X c= Y; theorem :: PBOOLE:51 Y c= X & X (/\) Y = EmptyMS I implies Y = EmptyMS I; begin :: Difference and symmetric difference theorem :: PBOOLE:52 X (\) Y = EmptyMS I iff X c= Y; theorem :: PBOOLE:53 X c= Y implies X (\) Z c= Y (\) Z; theorem :: PBOOLE:54 X c= Y implies Z (\) Y c= Z (\) X; theorem :: PBOOLE:55 X c= Y & Z c= V implies X (\) V c= Y (\) Z; theorem :: PBOOLE:56 X (\) Y c= X; theorem :: PBOOLE:57 X c= Y (\) X implies X = EmptyMS I; theorem :: PBOOLE:58 X (\) X = EmptyMS I; theorem :: PBOOLE:59 X (\) EmptyMS I = X; theorem :: PBOOLE:60 EmptyMS I (\) X = EmptyMS I; theorem :: PBOOLE:61 X (\) (X (\/) Y) = EmptyMS I; theorem :: PBOOLE:62 X (/\) (Y (\) Z) = (X (/\) Y) (\) Z; theorem :: PBOOLE:63 (X (\) Y) (/\) Y = EmptyMS I; theorem :: PBOOLE:64 X (\) (Y (\) Z) = (X (\) Y) (\/) X (/\) Z; theorem :: PBOOLE:65 (X (\) Y) (\/) X (/\) Y = X; theorem :: PBOOLE:66 X c= Y implies Y = X (\/) (Y (\) X); theorem :: PBOOLE:67 X (\/) (Y (\) X) = X (\/) Y; theorem :: PBOOLE:68 X (\) (X (\) Y) = X (/\) Y; theorem :: PBOOLE:69 X (\) (Y (/\) Z) = (X (\) Y) (\/) (X (\) Z); theorem :: PBOOLE:70 X (\) X (/\) Y = X (\) Y; theorem :: PBOOLE:71 X (/\) Y = EmptyMS I iff X (\) Y = X; theorem :: PBOOLE:72 (X (\/) Y) (\) Z = (X (\) Z) (\/) (Y (\) Z); theorem :: PBOOLE:73 (X (\) Y) (\) Z = X (\) (Y (\/) Z); theorem :: PBOOLE:74 (X (/\) Y) (\) Z = (X (\) Z) (/\) (Y (\) Z); theorem :: PBOOLE:75 (X (\/) Y) (\) Y = X (\) Y; theorem :: PBOOLE:76 X c= Y (\/) Z implies X (\) Y c= Z & X (\) Z c= Y; theorem :: PBOOLE:77 (X (\/) Y) (\) (X (/\) Y) = (X (\) Y) (\/) (Y (\) X); theorem :: PBOOLE:78 (X (\) Y) (\) Y = X (\) Y; theorem :: PBOOLE:79 X (\) (Y (\/) Z) = (X (\) Y) (/\) (X (\) Z); theorem :: PBOOLE:80 X (\) Y = Y (\) X implies X = Y; theorem :: PBOOLE:81 X (/\) (Y (\) Z) = X (/\) Y (\) X (/\) Z; theorem :: PBOOLE:82 X (\) Y c= Z implies X c= Y (\/) Z; theorem :: PBOOLE:83 X (\) Y c= X (\+\) Y; theorem :: PBOOLE:84 X (\+\) EmptyMS I = X; theorem :: PBOOLE:85 X (\+\) X = EmptyMS I; theorem :: PBOOLE:86 X (\/) Y = (X (\+\) Y) (\/) X (/\) Y; theorem :: PBOOLE:87 X (\+\) Y = (X (\/) Y) (\) X (/\) Y; theorem :: PBOOLE:88 (X (\+\) Y) (\) Z = (X (\) (Y (\/) Z)) (\/) (Y (\) (X (\/) Z)); theorem :: PBOOLE:89 X (\) (Y (\+\) Z) = X (\) (Y (\/) Z) (\/) X (/\) Y (/\) Z; theorem :: PBOOLE:90 (X (\+\) Y) (\+\) Z = X (\+\) (Y (\+\) Z); theorem :: PBOOLE:91 X (\) Y c= Z & Y (\) X c= Z implies X (\+\) Y c= Z; theorem :: PBOOLE:92 X (\/) Y = X (\+\) (Y (\) X); theorem :: PBOOLE:93 X (/\) Y = X (\+\) (X (\) Y); theorem :: PBOOLE:94 X (\) Y = X (\+\) (X (/\) Y); theorem :: PBOOLE:95 Y (\) X = X (\+\) (X (\/) Y); theorem :: PBOOLE:96 X (\/) Y = X (\+\) Y (\+\) X (/\) Y; theorem :: PBOOLE:97 X (/\) Y = X (\+\) Y (\+\) (X (\/) Y); begin :: Meeting and overlap(p?)ing theorem :: PBOOLE:98 X overlaps Y or X overlaps Z implies X overlaps Y (\/) Z; theorem :: PBOOLE:99 X overlaps Y & Y c= Z implies X overlaps Z; theorem :: PBOOLE:100 X overlaps Y & X c= Z implies Z overlaps Y; theorem :: PBOOLE:101 X c= Y & Z c= V & X overlaps Z implies Y overlaps V; theorem :: PBOOLE:102 X overlaps Y (/\) Z implies X overlaps Y & X overlaps Z; theorem :: PBOOLE:103 X overlaps Z & X c= V implies X overlaps Z (/\) V; theorem :: PBOOLE:104 X overlaps Y (\) Z implies X overlaps Y; theorem :: PBOOLE:105 Y does not overlap Z implies X (/\) Y does not overlap X (/\) Z; theorem :: PBOOLE:106 X overlaps Y (\) Z implies Y overlaps X (\) Z; theorem :: PBOOLE:107 X meets Y & Y c= Z implies X meets Z; theorem :: PBOOLE:108 Y misses X (\) Y; theorem :: PBOOLE:109 X (/\) Y misses X (\) Y; theorem :: PBOOLE:110 X (/\) Y misses X (\+\) Y; theorem :: PBOOLE:111 X misses Y implies X (/\) Y = EmptyMS I; theorem :: PBOOLE:112 X <> EmptyMS I implies X meets X; theorem :: PBOOLE:113 X c= Y & X c= Z & Y misses Z implies X = EmptyMS I; theorem :: PBOOLE:114 Z (\/) V = X (\/) Y & X misses Z & Y misses V implies X = V & Y = Z; theorem :: PBOOLE:115 X misses Y implies X (\) Y = X; theorem :: PBOOLE:116 X misses Y implies (X (\/) Y) (\) Y = X; theorem :: PBOOLE:117 X (\) Y = X implies X misses Y; theorem :: PBOOLE:118 X (\) Y misses Y (\) X; begin :: Roughly speaking definition let I,X,Y; pred X [= Y means :: PBOOLE:def 11 for x st x in X holds x in Y; reflexivity; end; theorem :: PBOOLE:119 X c= Y implies X [= Y; theorem :: PBOOLE:120 X [= Y & Y [= Z implies X [= Z; begin :: Non empty set of sorts theorem :: PBOOLE:121 EmptyMS {} in EmptyMS {}; theorem :: PBOOLE:122 for X being ManySortedSet of {} holds X = {}; reserve I for non empty set, x,X,Y for ManySortedSet of I; theorem :: PBOOLE:123 X overlaps Y implies X meets Y; theorem :: PBOOLE:124 not ex x st x in EmptyMS I; theorem :: PBOOLE:125 x in X & x in Y implies X (/\) Y <> EmptyMS I; theorem :: PBOOLE:126 X does not overlap EmptyMS I; theorem :: PBOOLE:127 X (/\) Y = EmptyMS I implies X does not overlap Y; theorem :: PBOOLE:128 X overlaps X implies X <> EmptyMS 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 12 for i being object st i in I holds X.i is empty; redefine attr X is non-empty means :: PBOOLE:def 13 for i being object st i in I holds X.i is non empty; end; registration let I be set; cluster empty-yielding for ManySortedSet of I; cluster non-empty for ManySortedSet of I; end; registration let I be non empty set; cluster non-empty -> non empty-yielding for ManySortedSet of I; cluster empty-yielding -> non non-empty for ManySortedSet of I; end; theorem :: PBOOLE:129 X is empty-yielding iff X = EmptyMS I; theorem :: PBOOLE:130 Y is empty-yielding & X c= Y implies X is empty-yielding; theorem :: PBOOLE:131 X is non-empty & X c= Y implies Y is non-empty; theorem :: PBOOLE:132 X is non-empty & X [= Y implies X c= Y; theorem :: PBOOLE:133 X is non-empty & X [= Y implies Y is non-empty; reserve X for non-empty ManySortedSet of I; theorem :: PBOOLE:134 ex x st x in X; theorem :: PBOOLE:135 (for x holds x in X iff x in Y) implies X = Y; theorem :: PBOOLE:136 (for x holds x in X iff x in Y & x in Z) implies X = Y (/\) Z; begin :: Addenda scheme :: PBOOLE:sch 3 MSSEx { I() -> set, P[object,object] }: ex f being ManySortedSet of I() st for i being object st i in I() holds P[i,f.i] provided for i being object st i in I() ex j being object st P[i,j]; scheme :: PBOOLE:sch 4 MSSLambda { I() -> set, F(object) -> object }: ex f being ManySortedSet of I() st for i being object st i in I() holds f.i = F(i); registration let I be set; cluster Function-yielding for ManySortedSet of I; end; definition let I be set; mode ManySortedFunction of I is Function-yielding ManySortedSet of I; end; theorem :: PBOOLE:137 not ex M being non-empty ManySortedSet of I st {} in rng M; definition let M be Function; mode Component of M is Element of rng M; end; theorem :: PBOOLE:138 for I being non empty set for M being ManySortedSet of I, A being Component of M ex i being object st i in I & A = M.i; theorem :: PBOOLE:139 for M being ManySortedSet of I, i st i in I holds M.i is Component of M; definition let I; let B be ManySortedSet of I; mode Element of B -> ManySortedSet of I means :: PBOOLE:def 14 for i being object st i in I holds it.i is Element of B.i; end; begin :: Many Sorted Functions definition let I; let A be ManySortedSet of I, B be ManySortedSet of I; mode ManySortedFunction of A,B -> ManySortedSet of I means :: PBOOLE:def 15 for i st i in I holds it.i is Function of A.i, B.i; end; registration let I; let A be ManySortedSet of I, B be ManySortedSet of I; cluster ->Function-yielding for ManySortedFunction of A,B; end; registration let I be set; let J be non empty set; let O be Function of I,J; let F be ManySortedSet of J; cluster F*O -> total for I-defined Function; end; reserve D for non empty set, n for Nat; scheme :: PBOOLE:sch 5 LambdaDMS {D()->non empty set, F(object)->object}: ex X be ManySortedSet of D() st for d be Element of D() holds X.d = F(d); registration let J be non empty set, B be non-empty ManySortedSet of J, j be Element of J; cluster B.j -> non empty; end; reserve X,Y for ManySortedSet of I; definition let I, X,Y; func [|X,Y|] -> ManySortedSet of I means :: PBOOLE:def 16 for i being object st i in I holds it.i = [:X.i,Y.i:]; end; definition let I, X, Y; func (Funcs) (X,Y) -> ManySortedSet of I means :: PBOOLE:def 17 for i being object st i in I holds it.i = Funcs(X.i,Y.i); end; definition let I be set, M be ManySortedSet of I; mode ManySortedSubset of M -> ManySortedSet of I means :: PBOOLE:def 18 it c= M; end; registration let I be set, M be non-empty ManySortedSet of I; cluster non-empty for ManySortedSubset of M; end; definition let F,G be Function-yielding Function; func G**F -> Function means :: PBOOLE:def 19 dom it = (dom F) /\ (dom G) & for i be object st i in dom it holds it.i = (G.i)*(F.i); end; registration let F,G be Function-yielding Function; cluster G**F -> Function-yielding; end; definition let I be set, A be ManySortedSet of I, F be ManySortedFunction of I; func F.:.:A -> ManySortedSet of I means :: PBOOLE:def 20 for i be set st i in I holds it.i = (F.i).:(A.i); end; registration let I; cluster EmptyMS I -> empty-yielding; end; scheme :: PBOOLE:sch 6 MSSExD { I() -> non empty set, P[object,object] }: ex f being ManySortedSet of I() st for i being Element of I() holds P[i,f.i] provided for i being Element of I() ex j being object st P[i,j]; registration let A be non empty set; cluster non-empty -> non empty-yielding for ManySortedSet of A; end; registration let X be non empty set; cluster -> non empty for ManySortedSet of X; end; theorem :: PBOOLE:140 for F, G, H be Function-yielding Function holds (H ** G) ** F = H ** (G ** F); registration let I be set, f be non-empty ManySortedSet of I; cluster total for I-defined f-compatible Function; end; theorem :: PBOOLE:141 for I being set, f being non-empty ManySortedSet of I for p being f-compatible I-defined Function ex s being f-compatible ManySortedSet of I st p c= s; theorem :: PBOOLE:142 for I,A be set for s,ss being ManySortedSet of I holds (ss +* s | A) | A = s | A; registration let X be non empty set, Y be set; cluster X-valued for ManySortedSet of Y; end; theorem :: PBOOLE:143 for I,Y being non empty set, M be Y-valued ManySortedSet of I, x be Element of I holds M.x = M/.x; theorem :: PBOOLE:144 for f being Function, M being ManySortedSet of I holds (f+*M)|I = M; theorem :: PBOOLE:145 for I being set, Y being non empty set for p being Y-valued I-defined Function ex s being Y-valued ManySortedSet of I st p c= s; theorem :: PBOOLE:146 X c= Y & Y c= X implies X = Y; definition let I be non empty set, A,B be ManySortedSet of I; redefine pred A = B means :: PBOOLE:def 21 for i being Element of I holds A.i = B.i; end; registration let X be with_non-empty_elements set; cluster id X -> non-empty; end; scheme :: PBOOLE:sch 7 MSSLambda { I() -> set, F(object) -> object }: ex f being ManySortedSet of I() st for i being set st i in I() holds f.i = F(i);