:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, SUBSET_1, XXREAL_0, CARD_1, ARYTM_3, RELAT_1, XBOOLE_0, METRIC_1, FUNCT_1, FCONT_2, PARTFUN1, PRE_TOPC, PCOMPS_1, ORDINAL2, RCOMP_1, ORDINAL1, STRUCT_0, TARSKI, SETFAM_1, FINSET_1, ZFMISC_1, TOPMETR, BORSUK_1, EUCLID, FINSEQ_1, ORDINAL4, COMPLEX1, ARYTM_1, XXREAL_1, VALUED_0, MEASURE5, NAT_1, INT_1, XXREAL_2, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SETFAM_1, COMPLEX1, REAL_1, NAT_D, INT_1, NAT_1, RCOMP_1, FUNCT_1, PARTFUN1, FINSEQ_1, RELSET_1, FUNCT_2, SEQM_3, STRUCT_0, TOPMETR, PRE_TOPC, TOPS_2, COMPTS_1, EUCLID, FINSET_1, TBSP_1, METRIC_1, PCOMPS_1; constructors REAL_1, RCOMP_1, TOPS_2, COMPTS_1, TBSP_1, TOPMETR, GOBOARD1, NAT_D, FUNCSDOM, PCOMPS_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, FINSEQ_1, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, BORSUK_2, VALUED_0, FUNCT_2, BORSUK_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: 1. Lebesgue's Covering Lemma reserve x,y for set; reserve s,s1,s2,s4,r,r1,r2 for Real; reserve n,m,i,j for Element of NAT; theorem :: UNIFORM1:1 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 Function of X,Y; attr f is uniformly_continuous means :: UNIFORM1:def 1 for r st 00 & u1=f.u ex s being Real st s>0 & for w being Element of N, w1 being Element of M st w1=f.w & dist(u,w)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)0 & for w1,w2 being Element of N st dist(w1,w2) IT.m; end; theorem :: UNIFORM1:13 for e being Real, g being Function of I[01],TOP-REAL n, p1,p2 being Element of TOP-REAL n st e>0 & g is continuous 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 & i0 & g is continuous 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