:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received November 13, 1997

:: Copyright (c) 1997-2021 Association of Mizar Users

:: deftheorem 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 ) ) );

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 Th2: :: UNIFORM1:2

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 M

for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds

f " P is open

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 M

for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds

f " P is open

proof end;

theorem Th3: :: UNIFORM1:3

for N, M being non empty MetrSpace

for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being Real

for u being Element 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 ) ) ) holds

f is continuous

for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being Real

for u being Element 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 ) ) ) holds

f is continuous

proof end;

theorem Th4: :: UNIFORM1:4

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

for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f is continuous holds

for r being Real

for u being Element 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:5

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

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;

:: Lebesgue's Covering Lemma

theorem Th6: :: UNIFORM1:6

for N being non empty MetrSpace

for G being Subset-Family of (TopSpaceMetr N) st G is 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 ) ) )

for G being Subset-Family of (TopSpaceMetr N) st G is 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 Th7: :: UNIFORM1:7

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

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

Lm2: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1))

by TOPMETR:20, TOPMETR:def 7;

Lm3: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1))

by Lm1, TOPMETR:12, TOPMETR:20;

theorem :: UNIFORM1:8

for n being Element of 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

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

proof end;

theorem :: UNIFORM1:9

for n being Element of 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

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 :: UNIFORM1:10

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;

Lm6: for r, s1, s2 being Real holds

( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )

proof end;

:: deftheorem 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 );

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 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:13

for n being Element of 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 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 ) )

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 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:14

for n being Element of 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 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 ) )

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