:: Functions and Finite Sequences of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received March 15, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem :: RFINSEQ:1
canceled;
theorem :: RFINSEQ:2
canceled;
theorem :: RFINSEQ:3
canceled;
theorem :: RFINSEQ:4
canceled;
theorem :: RFINSEQ:5
canceled;
theorem :: RFINSEQ:6
canceled;
theorem :: RFINSEQ:7
canceled;
theorem :: RFINSEQ:8
canceled;
theorem :: RFINSEQ:9
canceled;
theorem :: RFINSEQ:10
canceled;
theorem :: RFINSEQ:11
canceled;
theorem :: RFINSEQ:12
canceled;
theorem :: RFINSEQ:13
canceled;
theorem Th14: :: RFINSEQ:14
theorem :: RFINSEQ:15
theorem Th16: :: RFINSEQ:16
theorem Th17: :: RFINSEQ:17
defpred S1[ Nat] means for X being finite set
for F being Function st card (dom (F | X)) = $1 holds
ex a being FinSequence st F | X,a are_fiberwise_equipotent ;
Lm2:
S1[ 0 ]
Lm3:
for n being Element of NAT st S1[n] holds
S1[n + 1]
theorem :: RFINSEQ:18
:: deftheorem RFINSEQ:def 1 :
canceled;
:: deftheorem Def2 defines /^ RFINSEQ:def 2 :
Lm4:
for n being Nat
for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
theorem Th19: :: RFINSEQ:19
theorem Th20: :: RFINSEQ:20
theorem Th21: :: RFINSEQ:21
theorem :: RFINSEQ:22
:: deftheorem Def3 defines MIM RFINSEQ:def 3 :
theorem Th23: :: RFINSEQ:23
theorem Th24: :: RFINSEQ:24
theorem Th25: :: RFINSEQ:25
theorem Th26: :: RFINSEQ:26
theorem :: RFINSEQ:27
theorem :: RFINSEQ:28
theorem Th29: :: RFINSEQ:29
theorem :: RFINSEQ:30
:: deftheorem Def4 defines non-increasing RFINSEQ:def 4 :
theorem Th31: :: RFINSEQ:31
theorem Th32: :: RFINSEQ:32
theorem Th33: :: RFINSEQ:33
theorem :: RFINSEQ:34
Lm5:
for f, g being non-increasing FinSequence of REAL
for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds
( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent )
defpred S2[ Nat] means for R being FinSequence of REAL st $1 = len R holds
ex b being non-increasing FinSequence of REAL st R,b are_fiberwise_equipotent ;
Lm6:
S2[ 0 ]
Lm7:
for n being Element of NAT st S2[n] holds
S2[n + 1]
theorem :: RFINSEQ:35
Lm8:
for n being Element of NAT
for g1, g2 being non-increasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds
g1 = g2
theorem :: RFINSEQ:36
theorem :: RFINSEQ:37
theorem :: RFINSEQ:38
theorem :: RFINSEQ:39
theorem :: RFINSEQ:40
theorem :: RFINSEQ:41
theorem :: RFINSEQ:42
theorem Th9: :: RFINSEQ:43
theorem Th10: :: RFINSEQ:44
theorem :: RFINSEQ:45