Quellcode-Bibliothek ae_continuous_def.pvs

%------------------------------------------------------------------------------
% Definition of almost everywhere continuity
%
%     Author: David Lester, Manchester University
%
% References: AJ Weir, "Lebesgue Integration and Measure" CUP, 1973.
%
%     Version 1.0            26/2/10   Initial Version
%------------------------------------------------------------------------------

ae_continuous_def: THEORY

BEGIN

  IMPORTING
    lebesgue_def,
    measure_integration@indefinite_integral[real,cal_M,lambda_],
    metric_space@real_continuity

  a,b,x: VAR real
  f:     VAR [real->real]

  ae_continuous?(a:real,b:{x | a <= x},f):bool
    = null_set?({x | a < x AND x < b AND NOT continuous_at?(f,x)})

  ae_continuous_def: LEMMA a <= b =>
    (ae_continuous?(a,b,f) <=> ae_continuous?(a,b,phi(closed(a,b))*f))

  continuous_at_is_ae_continuous: LEMMA
    a <= b AND (FORALL x: a < x AND x < b => continuous_at?(f,x)) =>
    ae_continuous?(a,b,f)

  continuous_is_ae_continuous: LEMMA
    a <= b AND continuous?(f) => ae_continuous?(a,b,f)

END ae_continuous_def