The abstract of the Mizar article:

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

by

Yatsuka Nakamura, and

Andrzej Trybulec

Received November 13, 1997

MML identifier: UNIFORM1

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM_1, ARYTM_3, METRIC_1, PRE_TOPC, FINSEQ_4, PCOMPS_1, ORDINAL2,
      RELAT_1, FUNCT_1, BOOLE, SETFAM_1, COMPTS_1, FINSET_1, TARSKI, SUBSET_1,
      TOPMETR, BORSUK_1, EUCLID, INT_1, FINSEQ_1, ABSVALUE, RCOMP_1, SEQM_3,
      TBSP_1, SQUARE_1, LATTICES, UNIFORM1, HAHNBAN, ARYTM;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, SETFAM_1,
      REAL_1, NAT_1, ORDINAL1, INT_1, BINARITH, RCOMP_1, STRUCT_0, ABSVALUE,
      RELAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, FINSEQ_4, TOPMETR, PRE_TOPC, TOPS_2,
      COMPTS_1, EUCLID, FINSET_1, TBSP_1, PSCOMP_1, METRIC_1, PCOMPS_1,
      GOBOARD1, SQUARE_1;
 constructors RCOMP_1, ABSVALUE, TOPS_2, REAL_1, TOPMETR, INT_1, SQUARE_1,
      PSCOMP_1, BINARITH, TBSP_1, GOBOARD1, T_0TOPSP, YELLOW_8, FINSEQ_4,
      COMPTS_1;
 clusters SUBSET_1, STRUCT_0, RELSET_1, EUCLID, METRIC_1, PCOMPS_1, BORSUK_2,
      XREAL_0, FINSEQ_1, TOPMETR, INT_1, NAT_1, MEMBERED, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: 1.   LEBESGUE'S COVERING LEMMA

reserve x,y for set;
reserve s,s1,s2,s4,t,r,r1,r2 for Real;
reserve n,m,i,j for Nat;

theorem :: UNIFORM1:1
t-r-(t-s)=-r+s & t-r-(t-s)=s-r;

theorem :: UNIFORM1:2
for r st r>0 ex n being Nat st n>0 & 1/n < r;

definition let X,Y be non empty MetrStruct,f be map of X,Y;
 attr f is uniformly_continuous means
:: UNIFORM1:def 1
 for r st 0<r ex s st 0<s & for u1,u2 being Element of X
    st dist(u1,u2) < s holds dist(f/.u1,f/.u2) < r;
end;

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

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

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

theorem :: UNIFORM1:6
for N,M being non empty MetrSpace,
 f being map of N,M,
 g being map of TopSpaceMetr(N),TopSpaceMetr(M) st
 f=g & f is uniformly_continuous holds
 g is continuous;

reserve p for Nat;

theorem :: UNIFORM1:7  :: Lebesgue's Covering Lemma
  for N being non empty MetrSpace,
      G being Subset-Family of TopSpaceMetr(N) st
   G is_a_cover_of TopSpaceMetr(N) & G is open & TopSpaceMetr(N) is compact
ex r 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;

begin ::2.   UNIFORMITY OF CONTINUOUS FUNCTIONS ON COMPACT SPACES
theorem :: UNIFORM1:8
for N,M being non empty MetrSpace,f being map of N,M,
 g being map of TopSpaceMetr(N),TopSpaceMetr(M)
 st g=f & TopSpaceMetr(N) is compact & g is continuous
 holds f is uniformly_continuous;

theorem :: UNIFORM1:9
for g being map of I[01],TOP-REAL n, f being map of
 Closed-Interval-MSpace(0,1),Euclid n
 st g is continuous & f=g holds f is uniformly_continuous;

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

begin ::3.   SEGMENTATION OF ARCS
theorem :: UNIFORM1:11
for g being map of I[01],(TOP-REAL n)
  ex f being map of Closed-Interval-MSpace(0,1),Euclid n st f=g;

theorem :: UNIFORM1:12
for r being real number st r>=0 holds
[/ r \]>=0 & [\ r /]>=0 & [/ r \] is Nat & [\ r /] is Nat;

theorem :: UNIFORM1:13
for r,s holds abs(r-s)=abs(s-r);

theorem :: UNIFORM1:14
for r1,r2,s1,s2 st r1 in [.s1,s2.] & r2 in [.s1,s2.]
  holds abs(r1-r2)<=s2-s1;

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

theorem :: UNIFORM1:15
   for e being Real,g being map of I[01],TOP-REAL n,
   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
   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,Q being Subset of I[01],
    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);

theorem :: UNIFORM1:16
   for e being Real,g being map of I[01], (TOP-REAL n),
   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
   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,Q being Subset of I[01],
    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);