|
%------------------------------------------------------------------------------
% 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
[ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
]
|
