environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SEQ_1, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1, COMPLEX1, ORDINAL2, REAL_1, SEQ_4, RELAT_1, FUNCT_1, TARSKI, XXREAL_2, XBOOLE_0, SUPINF_2, PARTFUN3, NAT_1, VALUED_1, VALUED_0, SEQ_2, RINFSUP1, MEMBER_1;
notations HIDDEN, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, COMPLEX1, TARSKI, XXREAL_2, VALUED_0, FUNCT_1, SEQ_4, XBOOLE_0, SUBSET_1, COMSEQ_2, SEQ_2, RELSET_1, FUNCT_2, MEASURE6, VALUED_1, SEQ_1, PARTFUN3, MEMBER_1;
definitions TARSKI, XBOOLE_0, PARTFUN3, XXREAL_2;
theorems FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, NAT_1, TARSKI, XREAL_0, SEQ_4, SEQM_3, SETLIM_1, LIMFUNC1, PREPOWER, XREAL_1, XXREAL_0, ORDINAL1, RELAT_1, XXREAL_2, VALUED_0, MEASURE6, MEMBER_1;
schemes FUNCT_2, NAT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, RFUNCT_1, MEMBER_1, NAT_1;
constructors HIDDEN, REAL_1, NAT_1, COMPLEX1, SEQM_3, LIMFUNC1, PARTFUN3, PARTFUN1, XXREAL_2, SEQ_4, RELSET_1, BINOP_2, SEQ_2, MEASURE6, MEMBER_1, SQUARE_1, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities VALUED_1;
expansions TARSKI, XBOOLE_0, PARTFUN3, VALUED_1, XXREAL_2;
Lm1:
for r1, r2, s being Real st 0 < s & r1 <= r2 holds
( r1 < r2 + s & r1 - s < r2 )
theorem Th1:
for
r,
s,
t being
Real holds
( (
s - r < t &
s + r > t ) iff
|.(t - s).| < r )
Lm2:
for n being Nat
for seq being Real_Sequence st seq is V54() holds
(inferior_realsequence seq) . n = seq . n
Lm3:
for n being Nat
for seq being Real_Sequence st seq is V55() holds
(superior_realsequence seq) . n = seq . n