|
%------------------------------------------------------------------------------
% Linking real topology and borel sets
%
% Author: David Lester, Manchester University
%
% Version 1.0 17/08/07 Initial Version
% Version 1.1 23/03/11 Extras for probability
%------------------------------------------------------------------------------
real_borel: THEORY
BEGIN
IMPORTING metric_space@real_topology,
borel[real,metric_induced_topology],
hausdorff_borel[real,metric_induced_topology]
real_borel:sigma_algebra = (borel?)
borel_generated_by_rational_open_interval: LEMMA
borel? = generated_sigma_algebra(fullset[rational_open_interval])
borel_generated_by_open_interval: LEMMA
borel? = generated_sigma_algebra(fullset[open_interval])
% From borel and hausdorff_borel:
% singleton_is_borel: LEMMA borel?(singleton(x))
% singleton_is_borel_judge: JUDGEMENT singleton(x) HAS_TYPE 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))
A: VAR open_interval
B: VAR closed_interval
L: VAR left_semiclosed_interval
R: VAR right_semiclosed_interval
open_interval_borel_rew: LEMMA real_borel(A)
closed_interval_borel_rew: LEMMA real_borel(B)
left_semiclosed_interval_borel_rew: LEMMA real_borel(L)
right_semiclosed_interval_borel_rew: LEMMA real_borel(R)
AUTO_REWRITE+ open_interval_borel_rew
AUTO_REWRITE+ closed_interval_borel_rew
AUTO_REWRITE+ left_semiclosed_interval_borel_rew
AUTO_REWRITE+ right_semiclosed_interval_borel_rew
open_interval_is_borel: JUDGEMENT open_interval SUBTYPE_OF borel
closed_interval_is_borel: JUDGEMENT closed_interval SUBTYPE_OF borel
left_semiclosed_interval_is_borel:
JUDGEMENT left_semiclosed_interval SUBTYPE_OF borel
right_semiclosed_interval_is_borel:
JUDGEMENT right_semiclosed_interval SUBTYPE_OF borel
% IMPORTING sigma_algebra % Proof Only
borel_generated_by_left_semiclosed_interval: LEMMA
borel? = generated_sigma_algebra(fullset[left_semiclosed_interval])
borel_generated_by_right_semiclosed_interval: LEMMA
borel? = generated_sigma_algebra(fullset[right_semiclosed_interval])
END real_borel
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
