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