|
%-------------------------------------------------------------------------
% Measure Space Definitions
%
% Author: David Lester, Manchester University
%
% Version 1.0 04/05/09 Initial (DRL)
%-------------------------------------------------------------------------
measure_space_def[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra]: THEORY
BEGIN
IMPORTING sigma_algebra[T,S],
reals@real_fun_ops_aux[T],
structures@const_fun_def[T,real],
metric_space@real_topology,
topology@basis[real],
borel[real,metric_induced_topology],
real_borel,
sets_aux@countable_props,
sets_aux@inverse_image_Union, % Proof Only
sets_aux@countable_image, % Proof Only
sets_aux@countable_set % Proof Only
X: VAR set[T]
Y: VAR set[real]
x,y,z: VAR T
f: VAR [T->real]
B: VAR borel
c: VAR real
q: VAR rational
r: VAR posreal
measurable_set?(X):bool = S(X)
measurable_set: TYPE+ = (measurable_set?) CONTAINING emptyset[T]
a,b: VAR measurable_set
SS: VAR sequence[measurable_set]
M: VAR countable_set[(S)]
measurable_emptyset: JUDGEMENT emptyset[T] HAS_TYPE measurable_set
measurable_fullset: JUDGEMENT fullset[T] HAS_TYPE measurable_set
measurable_complement: JUDGEMENT complement(a) HAS_TYPE measurable_set
measurable_union: JUDGEMENT union(a,b) HAS_TYPE measurable_set
measurable_intersection: JUDGEMENT intersection(a,b) HAS_TYPE measurable_set
measurable_difference: JUDGEMENT difference(a,b) HAS_TYPE measurable_set
measurable_Union: JUDGEMENT Union(M) HAS_TYPE measurable_set
measurable_Intersection: JUDGEMENT Intersection(M) HAS_TYPE measurable_set
measurable_IUnion: JUDGEMENT IUnion(SS) HAS_TYPE measurable_set
measurable_IIntersection: JUDGEMENT IIntersection(SS) HAS_TYPE measurable_set
measurable_function?(f):bool = FORALL B: measurable_set?(inverse_image(f,B))
measurable_function: TYPE+ = (measurable_function?) CONTAINING (LAMBDA x: 0)
g,g1,g2: VAR measurable_function
measurable_is_function: JUDGEMENT measurable_function SUBTYPE_OF [T->real]
constant_is_measurable: JUDGEMENT (constant?[T,real]) SUBTYPE_OF
measurable_function
U: VAR setofsets[real]
measurable_def: LEMMA borel? = generated_sigma_algebra(U) =>
(measurable_function?(f) <=>
FORALL (X:(U)): S(inverse_image(f,X)))
measurable_def2: LEMMA measurable_function?(f) <=>
FORALL (i:open_interval): S(inverse_image(f,i))
measurable_gt: LEMMA measurable_function?(f) <=> FORALL c: S({z| f(z) > c})
measurable_le: LEMMA measurable_function?(f) <=> FORALL c: S({z| f(z) <= c})
measurable_lt: LEMMA measurable_function?(f) <=> FORALL c: S({z| f(z) < c})
measurable_ge: LEMMA measurable_function?(f) <=> FORALL c: S({z| f(z) >= c})
measurable_gt2: LEMMA measurable_function?(f) <=> FORALL q: S({z| f(z) > q})
measurable_le2: LEMMA measurable_function?(f) <=> FORALL q: S({z| f(z) <= q})
measurable_lt2: LEMMA measurable_function?(f) <=> FORALL q: S({z| f(z) < q})
measurable_ge2: LEMMA measurable_function?(f) <=> FORALL q: S({z| f(z) >= q})
scal_measurable: JUDGEMENT *(c,g) HAS_TYPE measurable_function
sum_measurable: JUDGEMENT +(g1,g2) HAS_TYPE measurable_function
opp_measurable: JUDGEMENT -(g) HAS_TYPE measurable_function
diff_measurable: JUDGEMENT -(g1,g2) HAS_TYPE measurable_function
END measure_space_def
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
