Quelle real_topology.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Metric Spaces
%
%     Author: David Lester, Manchester University, NIA, Universite Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            17/08/07  Initial Version
%     Version 1.1            23/03/11  New intervals added for probability
%------------------------------------------------------------------------------

real_topology: THEORY

BEGIN

  IMPORTING metric_space_def[real,(LAMBDA (x,y:real): abs(x-y))],
            metric_space[real,(LAMBDA (x,y:real): abs(x-y))],
            reals@bounded_reals,
            countable_cross[rat,posrat],    % Proof Only
            sets_aux@countable_types  % Proof only

  a,x,y: VAR real
  r:   VAR posreal
  q:   VAR rat
  pq:  VAR posrat
  X,A: VAR set[real]

  interval?(A):bool = FORALL (x,y:(A),z:real): x <= z AND z <= y => A(z)

  bounded?(A):bool
    = (empty?(A) OR
      (nonempty?(A) AND above_bounded[real](A) AND below_bounded[real](A)))

  unbounded?(A):bool = NOT bounded?(A)

  bounded_interval?(A):bool      = interval?(A) AND bounded?(A)
  unbounded_interval?(A):bool    = interval?(A) AND unbounded?(A)
  bounded_open_interval?(A):bool = bounded_interval?(A) and metric_open?(A)

  interval:           TYPE+ = (interval?)           CONTAINING emptyset[real]
  bounded_interval:   TYPE+ = (bounded_interval?)   CONTAINING emptyset[real]
  unbounded_interval: TYPE+ = (unbounded_interval?) CONTAINING fullset[real]
  bounded_open_interval:
                      TYPE+ = (bounded_open_interval?)CONTAINING emptyset[real]

  open_interval: TYPE+ = {X | EXISTS x,r: X = ball(x,r)}

  open_interval_is_bounded_open_interval:
            JUDGEMENT open_interval SUBTYPE_OF bounded_open_interval

  open_basis: LEMMA base?(metric_induced_topology)(fullset[open_interval])

  rational_open_interval: TYPE+ = {X | EXISTS q,pq: X = ball(q,pq)}

  rational_basis: LEMMA
               base?(metric_induced_topology)(fullset[rational_open_interval])

  countable_rational_open_interval: LEMMA
      is_countable(fullset[rational_open_interval])

  metric_induced_topology_is_second_countable:
                 JUDGEMENT metric_induced_topology HAS_TYPE second_countable

  real_is_complete: JUDGEMENT fullset[real] HAS_TYPE metric_complete

  closed_ball(x:real,r:nnreal):closed = {y | abs(x-y) <= r}

  closed_interval: TYPE+ = {X | EXISTS (x:real,r:nnreal): X = closed_ball(x,r)}

  open(a:real,b:{x | a < x}):   open_interval   = ball((a+b)/2,(b-a)/2)
  closed(a:real,b:{x | a <= x}):closed_interval = closed_ball((a+b)/2,(b-a)/2)

  open_inf(a):open = {x | a < x}
  inf_open(a):open = {x | x < a}

  reals:open    = fullset[real]
  posreals:open = open_inf(0)
  negreals:open = inf_open(0)

  closed_inf(a):closed = {x | a <= x}
  inf_closed(a):closed = {x | x <= a}

  nnreals:closed = closed_inf(0)
  npreals:closed = inf_closed(0)

  left_semiclosed_interval:  TYPE+ = {X | EXISTS a: X = closed_inf(a)}
                                     CONTAINING closed_inf(0)
  right_semiclosed_interval: TYPE+ = {X | EXISTS a: X = inf_closed(a)}
                                     CONTAINING inf_closed(0)

  left_semiclosed_interval_is_interval:
                        JUDGEMENT left_semiclosed_interval  SUBTYPE_OF interval
  right_semiclosed_interval_is_interval:
                        JUDGEMENT right_semiclosed_interval SUBTYPE_OF interval

  left_semiclosed_interval_is_closed:
                        JUDGEMENT left_semiclosed_interval  SUBTYPE_OF closed
  right_semiclosed_interval_is_closed:
                        JUDGEMENT right_semiclosed_interval SUBTYPE_OF closed

END real_topology

quality96%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.