Quellcode-Bibliothek real_borel.pvs Sprache: unbekannt

%------------------------------------------------------------------------------
% 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

quality94%

Quellcode-Bibliothek real_borel.pvs Sprache: unbekannt

[ 0.10Quellennavigators Projekt ]