%------------------------------------------------------------------------------
% Borel functions
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            1/05/07  Initial Version
%------------------------------------------------------------------------------
borel_functions[(IMPORTING topology@topology_def)
                T1:Type, S:topology[T1],
                T2:Type, T:topology[T2]]: THEORY

BEGIN

  IMPORTING borel,
            structures@const_fun_def[T1,T2],
            topology@continuity_def[T1,S,T2,T],
            topology@continuity[T1,S,T2,T]

  f: VAR [T1->T2]
  c: VAR T2
  X: VAR open[T2,T]
  B: VAR borel[T2,T]

  borel_function?(f):bool = (FORALL B: borel?[T1,S](inverse_image(f,B)))

  borel_function_def: LEMMA borel_function?(f) IFF
                            FORALL X: borel?[T1,S](inverse_image[T1,T2](f,X))

  borel_function: TYPE = (borel_function?)

  const_borel_function: LEMMA borel_function?(const_fun[T1,T2](c))

  continuous_is_borel: JUDGEMENT continuous SUBTYPE_OF borel_function

END borel_functions