continuous_functions_ax [ T : TYPE FROM real ] : THEORY BEGIN f, f1, f2 : VAR [T -> real] g : VAR [T -> nzreal] u : VAR real x, x0 : VAR T epsilon, delta : VAR posreal continuous(f, x0) : bool %--- equivalent definitions ---% continuity_def : AXIOM continuous(f, x0) IFF FORALL epsilon : EXISTS delta : FORALL x : abs(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon %------------------------------------------ % Operations preserving continuity at x0 %------------------------------------------ sum_continuous : AXIOM continuous(f1, x0) and continuous(f2, x0) implies continuous(f1 + f2, x0) diff_continuous : AXIOM continuous(f1, x0) and continuous(f2, x0) implies continuous(f1 - f2, x0) prod_continuous : AXIOM continuous(f1, x0) and continuous(f2, x0) implies continuous(f1 * f2, x0) const_continuous : AXIOM continuous(u, x0) scal_continuous : AXIOM continuous(f, x0) implies continuous(u * f, x0) opp_continuous : AXIOM continuous(f, x0) implies continuous(- f, x0) div_continuous : AXIOM continuous(f, x0) and continuous(g, x0) implies continuous(f/g, x0) inv_continuous : AXIOM continuous(g, x0) implies continuous(1/g, x0) identity_continuous : AXIOM continuous(I[T], x0) %--------------------------------------------- % Continuity of f in a subset of its domain %--------------------------------------------- E : VAR { S : setof[real] | subset?(S, T_pred) } F : VAR setof[real] continuous(f, E) : bool continuity_subset : AXIOM subset?(F, E) AND continuous(f, E) IMPLIES continuous(f, F) %--- Operation preserving continuity in E ---% sum_set_continuous : AXIOM continuous(f1, E) and continuous(f2, E) implies continuous(f1 + f2, E) diff_set_continuous : AXIOM continuous(f1, E) and continuous(f2, E) implies continuous(f1 - f2, E) prod_set_continuous : AXIOM continuous(f1, E) and continuous(f2, E) implies continuous(f1 * f2, E) const_set_continuous : AXIOM continuous(u, E) scal_set_continuous : AXIOM continuous(f, E) implies continuous(u * f, E) opp_set_continuous : AXIOM continuous(f, E) implies continuous(- f, E) div_set_continuous : AXIOM continuous(f, E) and continuous(g, E) implies continuous(f/g, E) inv_set_continuous : AXIOM continuous(g, E) implies continuous(1/g, E) identity_set_continuous : AXIOM continuous(I[T], E) %--------------------------------- % Continuity of f in its domain %--------------------------------- continuous(f) : bool = FORALL x0 : continuous(f, x0) continuous_def2 : AXIOM continuous(f) IFF continuous(f, T_pred) continuity_subset2 : AXIOM continuous(f) IMPLIES continuous(f, E) %--- Properties ---% continuous_fun: TYPE+ = { f | continuous(f) } nz_continuous_fun: TYPE = { g | continuous(g) } h, h1, h2: VAR continuous_fun h3: VAR nz_continuous_fun % sum_fun_continuous : JUDGEMENT +(h1, h2) HAS_TYPE continuous_fun % diff_fun_continuous : JUDGEMENT -(h1, h2) HAS_TYPE continuous_fun % prod_fun_continuous : JUDGEMENT *(h1, h2) HAS_TYPE continuous_fun % const_fun_continuous : JUDGEMENT K_conversion(u) HAS_TYPE continuous_fun % scal_fun_continuous : JUDGEMENT *(u, h) HAS_TYPE continuous_fun % opp_fun_continuous : JUDGEMENT -(h) HAS_TYPE continuous_fun % div_fun_continuous : JUDGEMENT /(h, h3) HAS_TYPE continuous_fun % id_fun_continuous : JUDGEMENT I[T] HAS_TYPE continuous_fun % inv_fun_continuous : AXIOM continuous(1/h3) END continuous_functions_ax