:: Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received November 13, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users begin theorem Th1: :: UNIFORM1:1 for r being Real st r > 0 holds ex n being Element of NAT st ( n > 0 & 1 / n < r ) proofend; definition let X, Y be non empty MetrStruct ; let f be Function of X,Y; attrf 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_:_ 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 proofend; 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 number for u being Element 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 proofend; 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 ) ) proofend; 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 proofend; :: [WP: ] 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 ) ) ) proofend; begin 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 proofend; 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 proofend; 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 proofend; begin 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 ) proofend; 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) ) proofend; theorem Th11: :: UNIFORM1:11 for r, s being real number holds abs (r - s) = abs (s - r) proofend; Lm6: for r, s1, s2 being Real holds ( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) ) proofend; theorem Th12: :: UNIFORM1:12 for r1, r2, s1, s2 being Real st r1 in [.s1,s2.] & r2 in [.s1,s2.] holds abs (r1 - r2) <= s2 - s1 proofend; definition let IT be FinSequence of REAL ; attrIT is decreasing means :Def2: :: 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 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 proofend; 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 proofend; 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 Element of 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 ) ) proofend; 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 Element of 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 ) ) proofend;