Quelle  metric_space.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Metric space
%
%     Author: David Lester, Manchester University
%
%     Version 1.0             5/12/04  Initial Version
%     Version 1.1            15/06/09  All Proofs discharged (DRL)
%------------------------------------------------------------------------------

metric_space[T:TYPE, (IMPORTING metric_def[T]) d:metric]: THEORY

BEGIN

  IMPORTING metric_def[T],
            topology@topology_def[T],
            metric_space_def[T,d]

  S:     VAR set[T]
  x,y,z: VAR T
  r:     VAR posreal

  metric_open_set:set[T]   = emptyset[T]
  metric_closed_set:set[T] = complement(metric_open_set)

  metric_zero:      LEMMA d(x,y) = 0 <=> x = y
  metric_symmetric: LEMMA d(x,y)  = d(y,x)
  metric_triangle:  LEMMA d(x,z) <= d(x,y) + d(y,z)
  metric_is_0:      LEMMA d(x,x) = 0
  ball_centre:      LEMMA member(x,ball(x,r))
  metric_open_ball: LEMMA metric_open?(ball(x,r))

  metric_open:   TYPE+ = (metric_open?)   CONTAINING metric_open_set
  metric_closed: TYPE+ = (metric_closed?) CONTAINING metric_closed_set

  ball_is_metric_open: JUDGEMENT ball(x,r) HAS_TYPE metric_open

  metric_space_is_topology?:  JUDGEMENT metric_induced_topology
                                                     HAS_TYPE (topology?)
  metric_space_is_hausdorff?: JUDGEMENT metric_induced_topology
                                                     HAS_TYPE (hausdorff?)
  metric_space_is_topology:
                           JUDGEMENT metric_induced_topology HAS_TYPE topology
  metric_space_is_hausdorff:
                           JUDGEMENT metric_induced_topology HAS_TYPE hausdorff

  IMPORTING topology@topology[T,(metric_induced_topology)]

  metric_open_def:   LEMMA metric_open?(S)   <=> open?(S)
  metric_closed_def: LEMMA metric_closed?(S) <=> closed?(S)

  metric_open_is_open:     JUDGEMENT metric_open   SUBTYPE_OF open
  open_is_metric_open:     JUDGEMENT open          SUBTYPE_OF metric_open
  metric_closed_is_closed: JUDGEMENT metric_closed SUBTYPE_OF closed
  closed_is_metric_closed: JUDGEMENT closed        SUBTYPE_OF metric_closed

  metric_adherent_iff_adherent: LEMMA
                        metric_adherent?(x,S) <=> adherent_point?(x,S)

  metric_closure_is_Cl: LEMMA metric_closure(S) = Cl(S)

  IMPORTING topology@hausdorff_convergence[T,(metric_induced_topology)],
            sets_aux@countable_setofsets, % proof only
            sets_aux@countable_image,     % proof only
            countable_cross                     % proof only

  u,v: VAR sequence[T]

  metric_convergence_def: LEMMA convergence?(u,x) <=> metric_converges_to(u,x)

  weierstrass_bolzano?:bool
    = FORALL u: EXISTS v: subseq?(v,u) AND metric_convergent?(v)

  compact_is_weierstrass_bolzano: LEMMA                            % SKB 6.1.11
        compact?(fullset[T]) => weierstrass_bolzano?

  cauchy_subseq_is_totally_bounded: LEMMA                          % SKB 6.1.17
        (FORALL u: EXISTS v: cauchy?(v) AND subseq?(v,u)) =>
        totally_bounded?(fullset[T])

  totally_bounded_is_separable: LEMMA                              % SKB 6.1.19
        totally_bounded?(fullset[T]) => separable?(fullset[T])

  separable_has_countable_basis: LEMMA                             % SKB 6.1.21
        separable?(fullset[T]) => has_countable_basis?(metric_induced_topology)

  IMPORTING topology@lindelof,               % Proof Only
            sets_aux@nat_indexed_sets[T],      % Proof Only
            sets_aux@countable_indexed_sets[T] % Proof Only

  compact_iff_convergent_subseq: LEMMA                             % SKB 6.1.23
        compact?(fullset[T]) <=> weierstrass_bolzano?

  totally_bounded_iff_cauchy_subseq: LEMMA                         % SKB 6.1.24
        totally_bounded?(fullset[T]) <=>
        FORALL u: EXISTS v: cauchy?(v) AND subseq?(v,u)

  compact_is_complete_totally_bounded: LEMMA                       % SKB 6.1.26
        compact?(fullset[T]) <=>
        metric_complete?(fullset[T]) AND totally_bounded?(fullset[T])

  metric_complete: TYPE = (complete_metric_space?[T,d])

END metric_space