environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, ORDINAL1;
theorems TARSKI, RCOMP_1, TOPMETR, TOPS_1, METRIC_1, FUNCT_1, FUNCT_2, TBSP_1, NAT_1, FINSEQ_3, FINSEQ_1, ABSVALUE, PRE_TOPC, TOPS_2, FINSEQ_4, GOBOARD6, PCOMPS_1, SETFAM_1, SUBSET_1, COMPTS_1, SEQ_4, HEINE, INT_1, JORDAN2B, XBOOLE_0, XBOOLE_1, XREAL_0, FINSEQ_2, XCMPLX_1, FINSET_1, XREAL_1, XXREAL_0, PARTFUN1, XXREAL_1, EUCLID, SEQM_3, ORDINAL1;
schemes FUNCT_2, DOMAIN_1, SUBSET_1, FINSEQ_1, NAT_1;
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;
constructors HIDDEN, REAL_1, RCOMP_1, TOPS_2, COMPTS_1, TBSP_1, TOPMETR, GOBOARD1, NAT_D, FUNCSDOM, PCOMPS_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XCMPLX_0;
expansions TARSKI;
theorem Th1:
for
r being
Real st
r > 0 holds
ex
n being
Nat st
(
n > 0 & 1
/ n < r )
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;
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) )
Lm6:
for r, s1, s2 being Real holds
( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )
Lm7:
for f being FinSequence of REAL st ( for k being 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 Nat st 1 <= k & k < len f holds
f /. k > f /. (k + 1) ) holds
f is decreasing