:: RFINSEQ semantic presentation

definition

let c₁, c₂ be Relation;
pred c₁,c₂ are_fiberwise_equipotent means :Def1: :: RFINSEQ:def 1
for b₁ being set holds Card (a₁ " {b₁}) = Card (a₂ " {b₁});
reflexivity ;
symmetry ;

end;

:: deftheorem Def1 defines are_fiberwise_equipotent RFINSEQ:def 1 :

Lemma2: for b₁ being Function
for b₂ being set st not b₂ in rng b₁ holds
b₁ " {b₂} = {}

proof end;

theorem Th1: :: RFINSEQ:1

for b₁, b₂ being Function st b₁,b₂ are_fiberwise_equipotent holds
rng b₁ = rng b₂

proof end;

theorem Th2: :: RFINSEQ:2

for b₁, b₂, b₃ being Function st b₁,b₂ are_fiberwise_equipotent & b₁,b₃ are_fiberwise_equipotent holds
b₂,b₃ are_fiberwise_equipotent

proof end;

theorem Th3: :: RFINSEQ:3

for b₁, b₂ being Function holds
( b₁,b₂ are_fiberwise_equipotent iff ex b₃ being Function st
( dom b₃ = dom b₁ & rng b₃ = dom b₂ & b₃ is one-to-one & b₁ = b₂ * b₃ ) )

proof end;

theorem Th4: :: RFINSEQ:4

for b₁, b₂ being Function holds
( b₁,b₂ are_fiberwise_equipotent iff for b₃ being set holds Card (b₁ " b₃) = Card (b₂ " b₃) )

proof end;

theorem Th5: :: RFINSEQ:5

for b₁ being non empty set
for b₂, b₃ being Function st rng b₂ c= b₁ & rng b₃ c= b₁ holds
( b₂,b₃ are_fiberwise_equipotent iff for b₄ being Element of b₁ holds Card (b₂ " {b₄}) = Card (b₃ " {b₄}) )

proof end;

theorem Th6: :: RFINSEQ:6

for b₁, b₂ being Function st dom b₁ = dom b₂ holds
( b₁,b₂ are_fiberwise_equipotent iff ex b₃ being Permutation of dom b₁ st b₁ = b₂ * b₃ )

proof end;

theorem Th7: :: RFINSEQ:7

for b₁, b₂ being Function st b₁,b₂ are_fiberwise_equipotent holds
Card (dom b₁) = Card (dom b₂)

proof end;

theorem Th8: :: RFINSEQ:8

canceled;

theorem Th9: :: RFINSEQ:9

for b₁, b₂ being finite Function holds
( b₁,b₂ are_fiberwise_equipotent iff for b₃ being set holds card (b₁ " b₃) = card (b₂ " b₃) ) by Th4;

theorem Th10: :: RFINSEQ:10

for b₁, b₂ being finite Function st b₁,b₂ are_fiberwise_equipotent holds
card (dom b₁) = card (dom b₂)

proof end;

theorem Th11: :: RFINSEQ:11

for b₁ being non empty set
for b₂, b₃ being finite Function st rng b₂ c= b₁ & rng b₃ c= b₁ holds
( b₂,b₃ are_fiberwise_equipotent iff for b₄ being Element of b₁ holds card (b₂ " {b₄}) = card (b₃ " {b₄}) ) by Th5;

theorem Th12: :: RFINSEQ:12

canceled;

theorem Th13: :: RFINSEQ:13

for b₁, b₂ being FinSequence holds
( b₁,b₂ are_fiberwise_equipotent iff for b₃ being set holds card (b₁ " b₃) = card (b₂ " b₃) ) by Th4;

theorem Th14: :: RFINSEQ:14

for b₁, b₂, b₃ being FinSequence holds
( b₁,b₂ are_fiberwise_equipotent iff b₁ ^ b₃,b₂ ^ b₃ are_fiberwise_equipotent )

proof end;

theorem Th15: :: RFINSEQ:15

for b₁, b₂ being FinSequence holds b₁ ^ b₂,b₂ ^ b₁ are_fiberwise_equipotent

proof end;

theorem Th16: :: RFINSEQ:16

for b₁, b₂ being FinSequence st b₁,b₂ are_fiberwise_equipotent holds
( len b₁ = len b₂ & dom b₁ = dom b₂ )

proof end;

theorem Th17: :: RFINSEQ:17

for b₁, b₂ being FinSequence holds
( b₁,b₂ are_fiberwise_equipotent iff ex b₃ being Permutation of dom b₂ st b₁ = b₂ * b₃ )

proof end;

registration

let c₁ be Function;
let c₂ be finite set ;
cluster a₁ | a₂ -> Function-like finite ;
coherence

proof end;

end;

defpred S₁[ Nat] means for b₁ being finite set
for b₂ being Function st card (dom (b₂ | b₁)) = a₁ holds
ex b₃ being FinSequence st b₂ | b₁,b₃ are_fiberwise_equipotent ;

Lemma10: S₁[0]

proof end;

Lemma11: for b₁ being Nat st S₁[b₁] holds
S₁[b₁ + 1]

proof end;

theorem Th18: :: RFINSEQ:18

for b₁ being Function
for b₂ being finite set ex b₃ being FinSequence st b₁ | b₂,b₃ are_fiberwise_equipotent

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
let c₃ be Nat;
func c₂ /^ c₃ -> FinSequence of a₁ means :Def2: :: RFINSEQ:def 2
( len a₄ = (len a₂) - a₃ & ( for b₁ being Nat st b₁ in dom a₄ holds
a₄ . b₁ = a₂ . (b₁ + a₃) ) ) if a₃ <= len a₂
otherwise a₄ = <*> a₁;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def2 defines /^ RFINSEQ:def 2 :

Lemma13: for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st len b₃ <= b₁ holds
b₃ | b₁ = b₃

proof end;

theorem Th19: :: RFINSEQ:19

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in Seg b₃ holds
( (b₂ | b₃) . b₄ = b₂ . b₄ & b₄ in dom b₂ )

proof end;

theorem Th20: :: RFINSEQ:20

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat
for b₄ being set st len b₂ = b₃ + 1 & b₄ = b₂ . (b₃ + 1) holds
b₂ = (b₂ | b₃) ^ <*b₄*>

proof end;

theorem Th21: :: RFINSEQ:21

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Nat holds (b₂ | b₃) ^ (b₂ /^ b₃) = b₂

proof end;

theorem Th22: :: RFINSEQ:22

for b₁, b₂ being FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent holds
Sum b₁ = Sum b₂

proof end;

definition

let c₁ be FinSequence of REAL ;
func MIM c₁ -> FinSequence of REAL means :Def3: :: RFINSEQ:def 3
( len a₂ = len a₁ & a₂ . (len a₂) = a₁ . (len a₁) & ( for b₁ being Nat st 1 <= b₁ & b₁ <= (len a₂) - 1 holds
a₂ . b₁ = (a₁ . b₁) - (a₁ . (b₁ + 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines MIM RFINSEQ:def 3 :

theorem Th23: :: RFINSEQ:23

for b₁ being FinSequence of REAL
for b₂ being Real
for b₃ being Nat st len b₁ = b₃ + 2 & b₁ . (b₃ + 1) = b₂ holds
MIM (b₁ | (b₃ + 1)) = ((MIM b₁) | b₃) ^ <*b₂*>

proof end;

theorem Th24: :: RFINSEQ:24

for b₁ being FinSequence of REAL
for b₂, b₃ being Real
for b₄ being Nat st len b₁ = b₄ + 2 & b₁ . (b₄ + 1) = b₂ & b₁ . (b₄ + 2) = b₃ holds
MIM b₁ = ((MIM b₁) | b₄) ^ <*(b₂ - b₃),b₃*>

proof end;

theorem Th25: :: RFINSEQ:25

MIM (<*> REAL ) = <*> REAL

proof end;

theorem Th26: :: RFINSEQ:26

for b₁ being Real holds MIM <*b₁*> = <*b₁*>

proof end;

theorem Th27: :: RFINSEQ:27

for b₁, b₂ being Real holds MIM <*b₁,b₂*> = <*(b₁ - b₂),b₂*>

proof end;

theorem Th28: :: RFINSEQ:28

for b₁ being FinSequence of REAL
for b₂ being Nat holds (MIM b₁) /^ b₂ = MIM (b₁ /^ b₂)

proof end;

theorem Th29: :: RFINSEQ:29

for b₁ being FinSequence of REAL st len b₁ <> 0 holds
Sum (MIM b₁) = b₁ . 1

proof end;

theorem Th30: :: RFINSEQ:30

for b₁ being FinSequence of REAL
for b₂ being Nat st 1 <= b₂ & b₂ < len b₁ holds
Sum (MIM (b₁ /^ b₂)) = b₁ . (b₂ + 1)

proof end;

definition

let c₁ be FinSequence of REAL ;
attr a₁ is non-increasing means :Def4: :: RFINSEQ:def 4
for b₁ being Nat st b₁ in dom a₁ & b₁ + 1 in dom a₁ holds
a₁ . b₁ >= a₁ . (b₁ + 1);

end;

:: deftheorem Def4 defines non-increasing RFINSEQ:def 4 :

registration

cluster non-increasing FinSequence of REAL ;
existence

proof end;

end;

theorem Th31: :: RFINSEQ:31

for b₁ being FinSequence of REAL st ( len b₁ = 0 or len b₁ = 1 ) holds
b₁ is non-increasing

proof end;

theorem Th32: :: RFINSEQ:32

for b₁ being FinSequence of REAL holds
( b₁ is non-increasing iff for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & b₂ < b₃ holds
b₁ . b₂ >= b₁ . b₃ )

proof end;

theorem Th33: :: RFINSEQ:33

for b₁ being non-increasing FinSequence of REAL
for b₂ being Nat holds b₁ | b₂ is non-increasing FinSequence of REAL

proof end;

theorem Th34: :: RFINSEQ:34

for b₁ being non-increasing FinSequence of REAL
for b₂ being Nat holds b₁ /^ b₂ is non-increasing FinSequence of REAL

proof end;

Lemma27: for b₁, b₂ being non-increasing FinSequence of REAL
for b₃ being Nat st len b₁ = b₃ + 1 & len b₁ = len b₂ & b₁,b₂ are_fiberwise_equipotent holds
( b₁ . (len b₁) = b₂ . (len b₂) & b₁ | b₃,b₂ | b₃ are_fiberwise_equipotent )

proof end;

defpred S₂[ Nat] means for b₁ being FinSequence of REAL st a₁ = len b₁ holds
ex b₂ being non-increasing FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent ;

Lemma28: S₂[0]

proof end;

Lemma29: for b₁ being Nat st S₂[b₁] holds
S₂[b₁ + 1]

proof end;

theorem Th35: :: RFINSEQ:35

for b₁ being FinSequence of REAL ex b₂ being non-increasing FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent

proof end;

Lemma30: for b₁ being Nat
for b₂, b₃ being non-increasing FinSequence of REAL st b₁ = len b₂ & b₂,b₃ are_fiberwise_equipotent holds
b₂ = b₃

proof end;

theorem Th36: :: RFINSEQ:36

for b₁, b₂ being non-increasing FinSequence of REAL st b₁,b₂ are_fiberwise_equipotent holds
b₁ = b₂

proof end;

theorem Th37: :: RFINSEQ:37

for b₁ being FinSequence of REAL
for b₂, b₃ being Real st b₂ <> 0 holds
b₁ " {(b₃ / b₂)} = (b₂ * b₁) " {b₃}

proof end;

theorem Th38: :: RFINSEQ:38

for b₁ being FinSequence of REAL holds (0 * b₁) " {0} = dom b₁

proof end;