Quellcode-Bibliothek continuous_on.pvs   Sprache: unbekannt

%------------------------------------------------------------------------------
% Continuity on subtypes of real
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            26/2/10   Initial Version
%------------------------------------------------------------------------------

continuous_on[T:TYPE FROM real]: THEORY

BEGIN

  IMPORTING metric_space@real_topology,
            topology@continuity_def[real,metric_induced_topology,
                                    real,metric_induced_topology]

  f: VAR [real -> real]
  x: VAR T

  continuous_on?(f):bool = FORALL x: continuous_at?(f,x)

  continuous_on: TYPE = (continuous_on?)

END continuous_on