Quelle  topological_convergence.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Topological convergence
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            06/09/06  Initial Version
%------------------------------------------------------------------------------

topological_convergence[T:TYPE,(IMPORTING topology_def[T])
                        S:topology[T]]: THEORY

BEGIN

  IMPORTING topology[T,S], sequences[T], reals@real_fun_preds[nat],
            subseq[T]

  U:       VAR open
  u,u1,u2: VAR sequence
  l:       VAR T
  a:       VAR T
  i,n:     VAR nat

  convergence?(u,l):bool
    = FORALL U: U(l) => EXISTS n: FORALL i: i >= n => U(u(i))

  accumulation?(u, a): bool =  FORALL U,n: U(a) => EXISTS i: i >= n AND U(u(i))

  convergent?(u): bool = EXISTS l: convergence?(u, l)

  tconvergent?(u): MACRO bool = convergent?(u)

  convergent: TYPE = (convergent?)

  v : VAR convergent

  limit(v):T = epsilon(LAMBDA l: convergence?(v, l))

  limit_lemma : LEMMA convergence?(v, limit(v))

  limit_accumulation : LEMMA convergence?(u, l) => accumulation?(u, l)

  convergence_subsequence : LEMMA
        convergence?(u1, l) AND subseq?(u2, u1) => convergence?(u2, l)

END topological_convergence