%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Properties of real numbers % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_facts : THEORY BEGIN %---------------------------------------- % More properties of archimedean field %---------------------------------------- archimedean2 : THEOREM FORALL (x : posreal) : EXISTS (a : posnat) : 1/a < x archimedean3 : THEOREM FORALL (x : nonneg_real) : (FORALL (a : posnat) : x <= 1/a) implies x = 0 %------------------------------------------------- % Every real is between two successive integers %------------------------------------------------- nat_interval : LEMMA FORALL (x : nonneg_real) : EXISTS (a : nat) : a <= x and x < a + 1 int_interval : PROPOSITION FORALL (x : real) : EXISTS (a : integer) : a <= x and x < a +1 %--------------------------------------- % Short cuts for lub and glb of sets %--------------------------------------- U: VAR (bounded_above?) V: VAR (bounded_below?) x, y: VAR real epsilon: VAR posreal lub_is_bound: LEMMA FORALL (x: (U)): x <= lub(U) lub_is_lub: LEMMA lub(U) <= y IFF FORALL (x: (U)): x <= y adherence_sup: LEMMA FORALL epsilon: EXISTS (x: (U)): lub(U) - epsilon < x glb_is_bound: LEMMA FORALL (x: (V)): glb(V) <= x glb_is_glb: LEMMA y <= glb(V) IFF FORALL (x: (V)): y <= x adherence_inf: LEMMA FORALL epsilon: EXISTS (x: (V)): x < glb(V) + epsilon END real_facts