|
%------------------------------------------------------------------------------
% Borel
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 1/05/07 Initial Version
%------------------------------------------------------------------------------
borel[T:TYPE, (IMPORTING topology@topology_def[T]) S:topology]: THEORY
BEGIN
IMPORTING subset_algebra_def[T],
topology@topology[T,S],
topology@basis[T],
sets_aux@countability
x: VAR T
X: VAR open
Y: VAR closed
Z: VAR set[T]
B: VAR (base?[T](S))
% A: VAR sigma_algebra
borel?:sigma_algebra = generated_sigma_algebra(fullset[open])
borel: TYPE+ = (borel?) CONTAINING emptyset[T]
IMPORTING sigma_algebra[T,(borel?)]
a,b: VAR borel
A: VAR countable_set[borel]
C: VAR set[borel]
emptyset_is_borel: LEMMA borel?(emptyset[T])
fullset_is_borel: LEMMA borel?(fullset[T])
open_is_borel: LEMMA borel?(X)
closed_is_borel: LEMMA borel?(Y)
complement_is_borel: LEMMA borel?(complement(a))
union_is_borel: LEMMA borel?(union(a,b))
intersection_is_borel: LEMMA borel?(intersection(a,b))
difference_is_borel: LEMMA borel?(difference(a,b))
Union_is_borel: LEMMA borel?(Union(A))
Complement_is_borel: LEMMA every(borel?,Complement(C))
Intersection_is_borel: LEMMA borel?(Intersection(A))
emptyset_is_borel_judge: JUDGEMENT emptyset[T] HAS_TYPE borel
fullset_is_borel_judge: JUDGEMENT fullset[T] HAS_TYPE borel
open_is_borel_judge: JUDGEMENT open SUBTYPE_OF borel
closed_is_borel_judge: JUDGEMENT closed SUBTYPE_OF borel
complement_is_borel_judge: JUDGEMENT complement(a) HAS_TYPE borel
union_is_borel_judge: JUDGEMENT union(a,b) HAS_TYPE borel
intersection_is_borel_judge: JUDGEMENT intersection(a,b) HAS_TYPE borel
difference_is_borel_judge: JUDGEMENT difference(a,b) HAS_TYPE borel
borel_basis: LEMMA generated_sigma_algebra(B)(Z) => borel?(Z)
borel_countable_basis: LEMMA is_countable(B) =>
borel? = generated_sigma_algebra(B)
END borel
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
