begin
theorem
canceled;
theorem Th2:
:: deftheorem Def1 defines uniformly_continuous UNIFORM1:def 1 :
for X, Y being non empty MetrStruct
for f being Function of X,Y holds
( f is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for u1, u2 being Element of X st dist (u1,u2) < s holds
dist ((f /. u1),(f /. u2)) < r ) ) );
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
begin
theorem Th8:
Lm1:
Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:def 8;
Lm2:
I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:27, TOPMETR:def 8;
Lm3:
the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1))
by Lm1, TOPMETR:16, TOPMETR:27;
theorem
theorem
begin
theorem
Lm4:
for x being set
for f being FinSequence holds
( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x )
Lm5:
for x being set
for f being FinSequence st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
theorem
canceled;
theorem Th13:
Lm6:
for r, s1, s2 being Real holds
( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )
theorem Th14:
:: deftheorem Def2 defines decreasing UNIFORM1:def 2 :
for IT being FinSequence of REAL holds
( IT is decreasing iff for n, m being Element of NAT st n in dom IT & m in dom IT & n < m holds
IT . n > IT . m );
Lm7:
for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) holds
f is increasing
Lm8:
for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k > f /. (k + 1) ) holds
f is decreasing
theorem
theorem