Quelle euclidean.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Metric Spaces for Vector[n]
%
%     Author: David Lester, Manchester University
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            17/08/07  Initial Version
%------------------------------------------------------------------------------
euclidean[n:posnat]: THEORY

BEGIN

  IMPORTING vectors@vectors[n],
            reals@sigma[below[n]],
            reals@sqrt,
            reals@bounded_reals,
            metric_def[Vector],
            metric_space_def

  X:     VAR set[Vector]
  x,y,z: VAR Vector
  i:     VAR below[n]
  r:     VAR posreal

  sigma_nnreal_eq_0: LEMMA FORALL (f:[below[n]->nnreal]):
          sigma(0,n-1,f) = 0 <=> (FORALL i: f(i) = 0)

  d1:metric   = LAMBDA x,y: sigma(0,n-1,(LAMBDA i: abs(x(i)-y(i))))

  d2:metric   = LAMBDA x,y: sqrt(sigma(0,n-1,(LAMBDA i: sq(x(i)-y(i)))))

  dinf:metric = LAMBDA x,y: max({z:nnreal | EXISTS i: abs(x(i)-y(i)) = z})

  euclidean_d1:   LEMMA metric_space?[Vector,d1](fullset[Vector])

  euclidean_d2:   LEMMA metric_space?[Vector,d2](fullset[Vector])

  euclidean_dinf: LEMMA metric_space?[Vector,dinf](fullset[Vector])

% We now show that R^n has a countable basis.

  Qn : TYPE+ = [Index->rat] CONTAINING zero

  Qn_is_Vector: JUDGEMENT Qn SUBTYPE_OF Vector

  q:     VAR Qn
  pq:    VAR posrat

  IMPORTING metric_space[Vector,d2],
            countable_cross,         % Proof Only
            sets_aux@countable_types % Proof only

  Qn_countable: LEMMA is_countable(fullset[Qn])

  balls: TYPE+ = {X | EXISTS x,r: X = ball(x,r)} CONTAINING
                                                     ball[Vector,d2](zero,1)

  rational_balls: TYPE+ = {X | EXISTS q,pq: X = ball[Vector,d2](q,pq)}
                                   CONTAINING ball[Vector,d2](zero,1)

  ball_basis: LEMMA base?(metric_induced_topology[Vector,d2])(fullset[balls])

% WAS:  Qn_dense: LEMMA dense_in?(fullset[Qn],fullset[Vector])

  Qn_dense: LEMMA dense_in?({x | EXISTS q: x=q},fullset[Vector])

  Qn_basis: LEMMA
             base?(metric_induced_topology[Vector,d2])(fullset[rational_balls])

  countable_rational_balls: LEMMA is_countable(fullset[rational_balls])

  euclidean_topology_is_second_countable:
        JUDGEMENT metric_induced_topology[Vector,d2] HAS_TYPE second_countable

  IMPORTING complete_product, % Proof only
            real_topology,    % Proof only
            vectors@vectors,  % Proof only
            reals@sigma       % Proof only

  euclidean_topology_is_complete:
        JUDGEMENT fullset[Vector[n]] HAS_TYPE metric_complete[Vector[n],d2]

END euclidean

quality96%

¤ Dauer der Verarbeitung: 0.13 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.