cont_vect2_real: THEORY %------------------------------------------------------------------------------ % Continuous functions [ Vect2 -> real] % % Author: Rick Butler NASA Langley Research Center 2/1/2009 % %------------------------------------------------------------------------------ BEGIN IMPORTING limit_vect2_realVAR [Vect2 -> real]VAR [Vect2 -> nzreal]VAR realVAR Vect2VAR posrealVAR nat%-------------------- % Continuity at x0 %-------------------- FORALL epsilon : EXISTS delta : FORALL x :IMPLIES abs(f(x) - f(x0)) < epsilonLEMMA IFF convergence(f, x0, f(x0))LEMMA IFF convergent?(f, x0)%------------------------------------------ % Operations preserving continuity at x0 %------------------------------------------ LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)IMPLIES continuous_vr?(f1 + f2, x0)LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)IMPLIES continuous_vr?(f1 - f2, x0)LEMMA continuous_vr?(f1, x0) AND continuous_vr?(f2, x0)IMPLIES continuous_vr?(f1 * f2, x0)LEMMA continuous_vr?(const_fun(u), x0)LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(u * f, x0)LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(- f, x0)LEMMA continuous_vr?(f, x0) AND continuous_vr?(g, x0) IMPLIES continuous_vr?(f/g, x0)LEMMA continuous_vr?(g, x0) IMPLIES continuous_vr?(1/g, x0)LEMMA continuous_vr?(f, x0) IMPLIES continuous_vr?(f^n, x0)%--------------------------------- % Continuity of f in its domain %--------------------------------- FORALL x0: continuous_vr?(f, x0)% ------------ Alternate forms and names for convenience --------------- LEMMA continuous_vr?(f1) AND continuous_vr?(f2)IMPLIES continuous_vr?(f1 + f2)LEMMA continuous_vr?(f1) AND continuous_vr?(f2)IMPLIES continuous_vr?(f1 - f2)LEMMA continuous_vr?(f1) AND continuous_vr?(f2)IMPLIES continuous_vr?(f1 * f2)LEMMA continuous_vr?(const_fun(u))LEMMA continuous_vr?(f) IMPLIES continuous_vr?(u * f)LEMMA continuous_vr?(f) IMPLIES continuous_vr?(-f)LEMMA continuous_vr?(f) AND continuous_vr?(g) IMPLIES continuous_vr?(f/g)LEMMA continuous_vr?(g) IMPLIES continuous_vr?(1/g)LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)%--- Properties ---% TYPE + = { f | continuous_vr?(f) }TYPE = { g | continuous_vr?(g) }VAR continuous_vr_funVAR nz_continuous_vr_funJUDGEMENT +(h1, h2) HAS_TYPE continuous_vr_funJUDGEMENT -(h1, h2) HAS_TYPE continuous_vr_funJUDGEMENT *(h1, h2) HAS_TYPE continuous_vr_funJUDGEMENT const_fun(u) HAS_TYPE continuous_vr_funJUDGEMENT *(u, h) HAS_TYPE continuous_vr_funJUDGEMENT -(h) HAS_TYPE continuous_vr_funJUDGEMENT /(h, h3) HAS_TYPE continuous_vr_funLEMMA continuous_vr?(1/h3)LEMMA continuous_vr?(f) IMPLIES continuous_vr?(f^n)END cont_vect2_realquality 92%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
