| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/lebesgue/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quellcode-Bibliothek real_intervals_aux.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Properties of real intervals % % Author: David Lester, Manchester University % % Version 1.0 26/2/10 Initial Version %------------------------------------------------------------------------------ real_intervals_aux: THEORY BEGIN IMPORTING metric_space@real_topology, reals@bounded_reals X,A: VAR set[real] b: VAR bounded_interval u: VAR unbounded_interval n: VAR nat r: VAR posreal nnr: VAR nnreal a,x: VAR real closed_interval?(A):bool = interval?(A) and metric_closed?(A) open_interval?(A):bool = interval?(A) and metric_open?(A) bounded_open_interval_def: LEMMA bounded_open_interval?(A) <=> empty?(A) OR EXISTS x,r: A = ball(x,r) unbounded_open_interval_def: LEMMA (unbounded?(A) AND open_interval?(A)) <=> (A = fullset[real] OR (EXISTS a: A = open_inf(a)) OR (EXISTS a: A = inf_open(a))) length(b):nnreal = IF empty?[real](b) THEN 0 ELSE sup(b)-inf(b) ENDIF % 2.1.1 length_closed: LEMMA nonempty?[real](b) => length(b) = length({x | inf(b) <= x AND x <= sup(b)}) length_open: LEMMA nonempty?[real](b) => length(b) = length({x | inf(b) < x AND x < sup(b)}) length_empty_rew: LEMMA length(emptyset[real]) = 0 length_closed_rew: LEMMA FORALL (b:{x|a<=x}): length({x | a <= x AND x <= b}) = b-a length_open_rew: LEMMA FORALL (b:{x|a<=x}): length({x | a < x AND x < b}) = b-a left_closed_right_open_interval?(A):bool = nonempty?(A) AND interval?(A) AND (above_bounded(A) => NOT A(sup(A))) AND (below_bounded(A) => A(inf(A))) left_closed_right_open_interval: TYPE+ = (left_closed_right_open_interval?) CONTAINING fullset[real] nonempty_interval?(A):bool = nonempty?(A) AND interval?(A) nonempty_interval: TYPE+ = (nonempty_interval?) CONTAINING fullset[real] END real_intervals_aux ¤ 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.0.10Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
