environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, XBOOLE_0;
theorems FINSEQ_1, NAT_1, FUNCT_1, FINSEQ_2, TARSKI, CARD_2, CARD_1, PARTFUN1, FINSET_1, FINSEQ_3, RFUNCT_1, RVSUM_1, ZFMISC_1, RFINSEQ, RFUNCT_3, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, FUNCOP_1, ORDINAL1, VALUED_1, CLASSES1, INT_1, XREAL_0;
schemes NAT_1, FINSEQ_1;
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;
constructors HIDDEN, REAL_1, NAT_1, FINSEQOP, RVSUM_1, RFINSEQ, RFUNCT_3, CLASSES1, RELSET_1, BINOP_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, FINSEQ_2, RELAT_1;
expansions TARSKI, XBOOLE_0;
Lm1:
for f being Function
for x being object st not x in rng f holds
f " {x} = {}
Lm2:
for D being non empty finite set
for A being FinSequence of bool D
for k being 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 )
Lm5:
for n being 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
for
C,
D being non
empty finite set for
F being
PartFunc of
D,
REAL 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
C,
D being non
empty finite set for
F being
PartFunc of
D,
REAL 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
C,
D being non
empty finite set for
F being
PartFunc of
D,
REAL 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
C,
D being non
empty finite set for
F being
PartFunc of
D,
REAL 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
C,
D being non
empty finite set for
F being
PartFunc of
D,
REAL 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) )