Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

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

Back to top