:: UNIFORM1 semantic presentation

theorem :: UNIFORM1:1

canceled;

theorem Th2: :: UNIFORM1:2

for r being Real st r > 0 holds
ex n being Nat st
( n > 0 & 1 / n < r )

proof end;

definition

let X, Y be non empty MetrStruct ;
let f be Function of X,Y;
attr f is uniformly_continuous means :Def1: :: UNIFORM1:def 1
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 ) );

end;

:: deftheorem Def1 defines uniformly_continuous UNIFORM1:def 1 :

theorem Th3: :: UNIFORM1:3

for X being non empty TopSpace
for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of the carrier of M
for P being Subset of (TopSpaceMetr M) st P = Ball u,r holds
f " P is open

proof end;

theorem Th4: :: UNIFORM1:4

for N, M being non empty MetrSpace
for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being real number
for u being Element of the carrier of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being real number st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist u,w < s holds
dist u1,w1 < r ) ) ) holds
f is continuous

proof end;

theorem Th5: :: UNIFORM1:5

for N, M being non empty MetrSpace
for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of the carrier of N
for u1 being Element of M st r > 0 & u1 = f . u holds
ex s being Real st
( s > 0 & ( for w being Element of N
for w1 being Element of M st w1 = f . w & dist u,w < s holds
dist u1,w1 < r ) )

proof end;

theorem :: UNIFORM1:6

for N, M being non empty MetrSpace
for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds
g is continuous

proof end;

theorem Th7: :: UNIFORM1:7

for N being non empty MetrSpace
for G being Subset-Family of (TopSpaceMetr N) st G is_a_cover_of TopSpaceMetr N & G is open & TopSpaceMetr N is compact holds
ex r being Real st
( r > 0 & ( for w1, w2 being Element of N st dist w1,w2 < r holds
ex Ga being Subset of (TopSpaceMetr N) st
( w1 in Ga & w2 in Ga & Ga in G ) ) )

proof end;

theorem Th8: :: UNIFORM1:8

for N, M being non empty MetrSpace
for f being Function of N,M
for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds
f is uniformly_continuous

proof end;

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 Th9: :: UNIFORM1:9

for n being Nat
for g being Function of I[01] ,(TOP-REAL n)
for f being Function of (Closed-Interval-MSpace 0,1),(Euclid n) st g is continuous & f = g holds
f is uniformly_continuous by Lm1, Th8, TOPMETR:27;

theorem :: UNIFORM1:10

for n being Nat
for P being Subset of (TOP-REAL n)
for Q being non empty Subset of (Euclid n)
for g being Function of I[01] ,((TOP-REAL n) | P)
for f being Function of (Closed-Interval-MSpace 0,1),((Euclid n) | Q) st P = Q & g is continuous & f = g holds
f is uniformly_continuous

proof end;

theorem Th11: :: UNIFORM1:11

for n being Nat
for g being Function of I[01] ,(TOP-REAL n) ex f being Function of (Closed-Interval-MSpace 0,1),(Euclid n) st f = g

proof end;

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 )

proof end;

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) )

proof end;

theorem :: UNIFORM1:12

canceled;

theorem Th13: :: UNIFORM1:13

for r, s being Real holds abs (r - s) = abs (s - r)

proof end;

Lm6: for r, s1, s2 being Real holds
( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )

proof end;

theorem Th14: :: UNIFORM1:14

for r1, r2, s1, s2 being Real st r1 in [.s1,s2.] & r2 in [.s1,s2.] holds
abs (r1 - r2) <= s2 - s1

proof end;

definition

let IT be FinSequence of REAL ;
attr IT is decreasing means :Def2: :: UNIFORM1:def 2
for n, m being Nat st n in dom IT & m in dom IT & n < m holds
IT . n > IT . m;

end;

:: deftheorem Def2 defines decreasing UNIFORM1:def 2 :

Lm7: for f being FinSequence of REAL st ( for k being Nat st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) holds
f is increasing

proof end;

Lm8: for f being FinSequence of REAL st ( for k being Nat st 1 <= k & k < len f holds
f /. k > f /. (k + 1) ) holds
f is decreasing

proof end;

theorem :: UNIFORM1:15

for n being Nat
for e being Real
for g being Function of I[01] ,(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous & g is one-to-one & g . 0 = p1 & g . 1 = p2 holds
ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) )

proof end;

theorem :: UNIFORM1:16

for n being Nat
for e being Real
for g being Function of I[01] ,(TOP-REAL n)
for p1, p2 being Element of (TOP-REAL n) st e > 0 & g is continuous & g is one-to-one & g . 0 = p1 & g . 1 = p2 holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )

proof end;