| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle real_facts.pvs Sprache: PVS |
|||||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28