Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: young.prf Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% 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.1 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.