%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Lemmas used for limits of product and inverse %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% epsilon_lemmas : THEORY BEGIN x1, x2, y1, y2 : VAR real e, e1, e2 : VAR posreal IMPORTING real_facts, absolute_value %--- Lemmas for product ---% prod_bound : LEMMA abs(x1 - y1) < e1 AND abs(x2 - y2) < e2 IMPLIES abs(x1 * x2 - y1 * y2) < e1 * e2 + abs(y1) * e2 + abs(y2) * e1 prod_epsilon : LEMMA EXISTS e1, e2 : e1 * e2 + abs(y1) * e2 + abs(y2) * e1 < e %--- Lemmas for inverse ---% inv_bound : LEMMA abs(x1 - y1) < e1 and e1 < abs(y1) and x1 /= 0 and y1 /= 0 IMPLIES abs(1/x1 - 1/y1) < e1 / (abs(y1) * (abs(y1) - e1)) inv_epsilon1 : LEMMA y1 /= 0 IMPLIES EXISTS e1 : e1 < abs(y1) and e1 < e * (abs(y1) - e1) inv_epsilon : LEMMA y1 /= 0 IMPLIES EXISTS e1 : e1 < abs(y1) and e1 / (abs(y1) * (abs(y1) - e1)) < e END epsilon_lemmas