:: Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received November 13, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem :: UNIFORM1:1
canceled;
theorem Th2: :: UNIFORM1:2
:: deftheorem Def1 defines uniformly_continuous UNIFORM1:def 1 :
theorem Th3: :: UNIFORM1:3
theorem Th4: :: UNIFORM1:4
theorem Th5: :: UNIFORM1:5
theorem :: UNIFORM1:6
theorem Th7: :: UNIFORM1:7
theorem Th8: :: UNIFORM1:8
Lm1:
Closed-Interval-TSpace 0 ,1 = TopSpaceMetr (Closed-Interval-MSpace 0 ,1)
by TOPMETR:def 8;
Lm2:
I[01] = TopSpaceMetr (Closed-Interval-MSpace 0 ,1)
by TOPMETR:27, TOPMETR:def 8;
Lm3:
the carrier of I[01] = the carrier of (Closed-Interval-MSpace 0 ,1)
by Lm1, TOPMETR:16, TOPMETR:27;
theorem :: UNIFORM1:9
theorem :: UNIFORM1:10
theorem Th11: :: UNIFORM1:11
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 )
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) )
theorem :: UNIFORM1:12
canceled;
theorem Th13: :: UNIFORM1:13
Lm6:
for r, s1, s2 being Real holds
( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )
theorem Th14: :: UNIFORM1:14
:: deftheorem Def2 defines decreasing UNIFORM1:def 2 :
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
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
theorem :: UNIFORM1:15
theorem :: UNIFORM1:16