:: Introduction to Theory of Rearrangment :: by Yuji Sakai and Jaros{\l}aw Kotowicz :: :: Received May 22, 1993 :: Copyright (c) 1993-2021 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 NUMBERS, SUBSET_1, REAL_1, XBOOLE_0, MEMBERED, PARTFUN1, VALUED_1, FUNCT_1, RELAT_1, FINSEQ_1, NAT_1, XXREAL_0, FINSET_1, CARD_1, ARYTM_1, TARSKI, ARYTM_3, ZFMISC_1, ORDINAL4, RFINSEQ, RFUNCT_3, CLASSES1, CARD_3, PBOOLE, FINSEQ_2, FUNCT_3, VALUED_0, REARRAN1, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MEMBERED, FUNCT_1, RELSET_1, CARD_1, FINSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, NAT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, VALUED_1, RFUNCT_1, FINSEQOP, RVSUM_1, CLASSES1, RFINSEQ, RFUNCT_3; constructors REAL_1, NAT_1, FINSEQOP, RVSUM_1, RFINSEQ, RFUNCT_3, CLASSES1, RELSET_1, BINOP_2; registrations SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, VALUED_0, CARD_1, FINSEQ_2, FUNCT_1, INT_1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve n,m,k for Nat, x,y for set, r for Real; definition let D be non empty set, E be real-membered set, F be PartFunc of D,E, r be Real; redefine func r(#)F -> Element of PFuncs(D,REAL); end; definition let IT be FinSequence; attr IT is terms've_same_card_as_number means :: REARRAN1:def 1 for n be Nat st 1<=n & n<=len IT for B being finite set st B = IT.n holds card B = n; attr IT is ascending means :: REARRAN1:def 2 for n be Nat st 1<=n & n<=len IT - 1 holds IT.n c= IT.(n+1); end; definition let X be set; let IT be FinSequence of X; attr IT is length_equal_card_of_set means :: REARRAN1:def 3 ex B being finite set st B = union X & len IT = card B; end; registration let D be non empty finite set; cluster terms've_same_card_as_number ascending length_equal_card_of_set for FinSequence of bool(D); end; definition let D be non empty finite set; mode RearrangmentGen of D is terms've_same_card_as_number ascending length_equal_card_of_set FinSequence of bool(D); end; reserve C,D for non empty finite set, a for FinSequence of bool D; theorem :: REARRAN1:1 for a be FinSequence of bool D holds a is length_equal_card_of_set iff len a = card D; theorem :: REARRAN1:2 for a be FinSequence holds a is ascending iff for n,m st n<=m & n in dom a & m in dom a holds a.n c= a.m; theorem :: REARRAN1:3 for a be terms've_same_card_as_number length_equal_card_of_set FinSequence of bool D holds a.(len a) = D; theorem :: REARRAN1:4 for a be length_equal_card_of_set FinSequence of bool D holds len a <> 0; theorem :: REARRAN1:5 for a be ascending terms've_same_card_as_number FinSequence of bool D holds for n,m holds n in dom a & m in dom a & n<>m implies a.n <> a.m; theorem :: REARRAN1:6 for a be ascending terms've_same_card_as_number FinSequence of bool D holds for n holds 1 <= n & n <= len a - 1 implies a.n <> a.(n+1); theorem :: REARRAN1:7 for a be terms've_same_card_as_number FinSequence of bool D st n in dom a holds a.n <> {}; theorem :: REARRAN1:8 for a be terms've_same_card_as_number FinSequence of bool D st 1 <=n & n<=len a - 1 holds a.(n+1) \ a.n <> {}; theorem :: REARRAN1:9 for a be terms've_same_card_as_number length_equal_card_of_set FinSequence of bool D ex d be Element of D st a.1 = {d}; theorem :: REARRAN1:10 for a be terms've_same_card_as_number ascending FinSequence of bool D st 1<=n & n<=len a - 1 ex d be Element of D st a.(n+1) \ a.n = {d} & a.( n+1) = a.n \/ {d} & a.(n+1) \ {d} = a.n; definition let D be non empty finite set, A be RearrangmentGen of D; func Co_Gen A -> RearrangmentGen of D means :: REARRAN1:def 4 for m be Nat st 1 <= m & m <= len it - 1 holds it.m = D \ A.(len A -m); involutiveness; end; ::$CT theorem :: REARRAN1:12 for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total & card C = card D holds len MIM FinS(F,D) = len CHI(A,C); definition let D,C be non empty finite set, A be RearrangmentGen of C, F be PartFunc of D,REAL; func Rland (F,A) -> PartFunc of C,REAL equals :: REARRAN1:def 5 Sum (MIM(FinS(F,D)) (#) CHI(A, C)); func Rlor(F,A) -> PartFunc of C,REAL equals :: REARRAN1:def 6 Sum (MIM(FinS(F,D)) (#) CHI( Co_Gen A,C)); end; theorem :: REARRAN1:13 for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total & card C = card D holds dom Rland(F,A) = C; theorem :: REARRAN1:14 for c be Element of C, F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total & card C = card D holds (c in A.1 implies ( MIM(FinS(F,D)) (#) CHI(A,C))#c = MIM(FinS(F,D))) & for n st 1<=n & n (0 qua Real)) ^ (MIM(FinS(F,D)/^n)); theorem :: REARRAN1:15 for c be Element of C, F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total & card C = card D holds (c in A.1 implies ( Rland(F,A)).c = FinS(F,D).1) & for n st 1<=n & n