Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/Sources/formale Sprachen/PVS/measure_integration/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 2 kB image not shown  

Quellcode-Bibliothek real_borel.pvs   Sprache: PVS

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

94%


¤ 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.0.10Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.