begin
Lm1:
for f being Function
for x being set st not x in rng f holds
f " {x} = {}
:: deftheorem Def1 defines terms've_same_card_as_number REARRAN1:def 1 :
:: deftheorem Def2 defines ascending REARRAN1:def 2 :
Lm2:
for D being non empty finite set
for A being FinSequence of bool D
for k being Element of NAT st 1 <= k & k <= len A holds
A . k is finite
Lm3:
for D being non empty finite set
for A being FinSequence of bool D st len A = card D & A is terms've_same_card_as_number holds
for B being finite set st B = A . (len A) holds
B = D
Lm4:
for D being non empty finite set ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number )
:: deftheorem Def3 defines lenght_equal_card_of_set REARRAN1:def 3 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
Lm5:
for n being Element of NAT
for D being non empty finite set
for a being FinSequence of bool D st n in dom a holds
a . n c= D
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem Def4 defines Co_Gen REARRAN1:def 4 :
theorem
theorem Th12:
definition
let D,
C be non
empty finite set ;
let A be
RearrangmentGen of
C;
let F be
PartFunc of ,;
func Rland F,
A -> PartFunc of ,
equals
Sum ((MIM (FinS F,D)) (#) (CHI A,C));
correctness
coherence
Sum ((MIM (FinS F,D)) (#) (CHI A,C)) is PartFunc of ,;
;
func Rlor F,
A -> PartFunc of ,
equals
Sum ((MIM (FinS F,D)) (#) (CHI (Co_Gen A),C));
correctness
coherence
Sum ((MIM (FinS F,D)) (#) (CHI (Co_Gen A),C)) is PartFunc of ,;
;
end;
:: deftheorem defines Rland REARRAN1:def 5 :
:: deftheorem defines Rlor REARRAN1:def 6 :
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem
for
D,
C being non
empty finite set for
F being
PartFunc of ,
for
A being
RearrangmentGen of
C st
F is
total &
card C = card D holds
(
Rlor F,
A,
Rland F,
A are_fiberwise_equipotent &
FinS (Rlor F,A),
C = FinS (Rland F,A),
C &
Sum (Rlor F,A),
C = Sum (Rland F,A),
C )
theorem
for
r being
Real for
D,
C being non
empty finite set for
F being
PartFunc of ,
for
A being
RearrangmentGen of
C st
F is
total &
card C = card D holds
(
max+ ((Rland F,A) - r),
max+ (F - r) are_fiberwise_equipotent &
FinS (max+ ((Rland F,A) - r)),
C = FinS (max+ (F - r)),
D &
Sum (max+ ((Rland F,A) - r)),
C = Sum (max+ (F - r)),
D )
theorem
for
r being
Real for
D,
C being non
empty finite set for
F being
PartFunc of ,
for
A being
RearrangmentGen of
C st
F is
total &
card C = card D holds
(
max- ((Rland F,A) - r),
max- (F - r) are_fiberwise_equipotent &
FinS (max- ((Rland F,A) - r)),
C = FinS (max- (F - r)),
D &
Sum (max- ((Rland F,A) - r)),
C = Sum (max- (F - r)),
D )
theorem Th31:
theorem
theorem
theorem
for
r being
Real for
D,
C being non
empty finite set for
F being
PartFunc of ,
for
A being
RearrangmentGen of
C st
F is
total &
card C = card D holds
(
max+ ((Rlor F,A) - r),
max+ (F - r) are_fiberwise_equipotent &
FinS (max+ ((Rlor F,A) - r)),
C = FinS (max+ (F - r)),
D &
Sum (max+ ((Rlor F,A) - r)),
C = Sum (max+ (F - r)),
D )
theorem
for
r being
Real for
D,
C being non
empty finite set for
F being
PartFunc of ,
for
A being
RearrangmentGen of
C st
F is
total &
card C = card D holds
(
max- ((Rlor F,A) - r),
max- (F - r) are_fiberwise_equipotent &
FinS (max- ((Rlor F,A) - r)),
C = FinS (max- (F - r)),
D &
Sum (max- ((Rlor F,A) - r)),
C = Sum (max- (F - r)),
D )
theorem Th36:
theorem
theorem
theorem