environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, NAT_1, XBOOLE_0, XXREAL_0, FINSET_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, SEQ_1, FUNCT_1, VALUED_1, RELAT_1, SEQ_2, ORDINAL2, COMPLEX1, LIMFUNC1, FUNCT_2, INT_1, POWER, NEWTON, ASYMPT_0, FUNCT_7, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_1, FUNCT_2, XXREAL_0, XXREAL_2, INT_1, NAT_1, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, NEWTON, POWER, FUNCOP_1, FINSET_1, LIMFUNC1;
definitions TARSKI, FUNCT_1;
theorems TARSKI, FUNCT_2, INT_1, NAT_1, SEQ_1, SEQ_2, ABSVALUE, LIMFUNC1, POWER, PRE_FF, XREAL_0, XBOOLE_0, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_2;
schemes FUNCT_2, FINSEQ_1, NAT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, POWER, XXREAL_2, FUNCT_1, NEWTON;
constructors HIDDEN, REAL_1, NAT_1, SEQ_2, LIMFUNC1, NEWTON, POWER, VALUED_1, PARTFUN1, XXREAL_2, RELSET_1, FUNCOP_1, COMSEQ_2, SQUARE_1, SEQ_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1;
expansions ;
reconsider jj = 1, dwa = 2 as Element of REAL by XREAL_0:def 1;
Lm1:
for f, g being Real_Sequence
for n being Nat holds (f /" g) . n = (f . n) / (g . n)
Lm2:
for f, g being eventually-nonnegative Real_Sequence holds
( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g )
Lm3:
for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds
f in Big_Oh g