|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Properties of real numbers %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
real_facts : THEORY
BEGIN
S: VAR (nonempty?[real])
bounded?_lem : LEMMA bounded?(S) IFF
EXISTS (B: real): FORALL (x: (S)): abs(x) <= B
%----------------------------------------
% 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 : LEMMA
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?)
a,b,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
lub_closed_intv: LEMMA a < b IMPLIES lub({x | a <= x AND x <= b}) = b
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
glb_closed_intv: LEMMA a < b IMPLIES glb({x | a <= x AND x <= b}) = a
adherence_inf: LEMMA
FORALL epsilon: EXISTS (x: (V)): x < glb(V) + epsilon
END real_facts
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
