UNIFORM1: Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs

:: Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received November 13, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users

theorem Th1: :: UNIFORM1:1

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 :: 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 defines uniformly_continuous UNIFORM1:def 1 :

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

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

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

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

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

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

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

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

proof end;

theorem :: UNIFORM1:10

for n being Element of NAT
for g being Function of I[01],(TOP-REAL n) holds g is Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by Lm3, EUCLID:67;

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 Th11: :: UNIFORM1:11

for r, s being Real holds |.(r - s).| = |.(s - r).|

proof end;

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

proof end;

theorem Th12: :: UNIFORM1:12

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

proof end;

definition

let IT be FinSequence of REAL ;

attr IT is decreasing means :: UNIFORM1:def 2
for n, m being Element of NAT st n in dom IT & m in dom IT & n < m holds
IT . n > IT . m;

end;

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

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

proof end;