List of theorems referencing the symbol RECAUCHY
(875) Theorem 722a: [Every real Cauchy sequence can be approximated by a rational sequence] (F in ReCauchy) •imp (Ra_approx(F) in {g in RaCauchy | Ra_apseq(F,g)})
(876) Theorem 722b: [Every real Cauchy sequence has a real limit] (F in ReCauchy) •imp ((Ra_approx(F) in RaCauchy) & (Ra_approx(F) in RaSeq) & Ra_apseq(F,Ra_approx(F)) & (limit(F) in Re))
(877) Theorem 722: [The limit of a real Cauchy sequence is the real defined by any of its rational approximations] ((F in ReCauchy) & (G in RaSeq) & Ra_apseq(F,G)) •imp ((G in RaCauchy) & (Cauchy_to_Re(G) = limit(F)))
(878) Theorem 723: [The elementary operations on reals map Cauchy sequences into Cauchy sequences] ((F in ReCauchy) & (G in ReCauchy) & (Fp in RaCauchy) & (Gp in RaCauchy) & Ra_apseq(F,Fp) & Ra_apseq(G,Gp)) •imp ((((F •Res_PLUS G in ReCauchy) & Ra_apseq(F •Res_PLUS G,Fp •Ras_PLUS Gp))) & (((F •Res_MINUS G in ReCauchy) & Ra_apseq(F •Res_MINUS G,Fp •Ras_MINUS Gp))) & (((F •Res_TIMES G in ReCauchy) & Ra_apseq(F •Res_TIMES G,Fp •Ras_TIMES Gp))))
(879) Theorem 724: [The limit of a sum is the sum of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_PLUS G) = (limit(F) •R_PLUS limit(G)))
(880) Theorem 725: [The limit of a difference is the difference of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_MINUS G) = limit(F) •R_MINUS limit(G))
(881) Theorem 726: [The limit of a product is the product of limits] ((F in ReCauchy) & (G in ReCauchy)) •imp (limit(F •Res_TIMES G) = limit(F) •R_TIMES limit(G))
(882) Theorem 727: [The limit of a quotient is the quotient of limits, provided that the denominator limit is non-zero] ((F in ReCauchy) & (G in ReCauchy) & (limit(G) /= R_0)) •imp (limit(F •Res_OVER G) = limit(F) •R_OVER limit(G))
(892) Theorem 737: [Every real Cauchy sequence is approximated by a rational Cauchy sequence] (F in ReCauchy) •imp (EXISTS g in RaCauchy | Ra_apseq(F,g))
(893) Theorem 738: [Any two approximating rational sequences for a given real Cauchy sequence are equivalent] ((F in ReCauchy) & Ra_apseq(F,G) & Ra_apseq(F,GP)) •imp ((G in RaCauchy) & (GP in RaCauchy) & (Cauchy_to_Re(G) = Cauchy_to_Re(GP)))
(904) Theorem 749: [Continuous functions map limits into limits] (Cf_RR(F,S) & (G in ReCauchy) & (range(G) •incin S)) •imp ((F @ G in ReCauchy) & (limit(F @ G) = F~[limit(G)]))