Quellcode-Bibliothek open_sets.pvs Sprache: PVS

open_sets[T: TYPE FROM real]: THEORY
BEGIN

   AUTO_REWRITE+ member

   x,y: VAR T
   S,S1,S2: VAR set[T]
   open_ball?(x,S): bool = (EXISTS (delta: posreal):
                                (FORALL y: abs(x-y) < delta IMPLIES S(y)))

   r: VAR posreal
   open_ball(x,r): set[T] = {y: T | abs(x-y) < r}

   open_ball?_lem: LEMMA open_ball?(x,S) IFF
                           EXISTS r: subset?(open_ball(x,r),S)

   open?(S): bool = FORALL (x: (S)): open_ball?(x,S)

   open?_lem: LEMMA open?(S) AND S(x) IMPLIES open_ball?(x,S)

   closed?(S): bool = open?(complement(S))

   Open  : TYPE = (open?)      %% = {S: set[T] | open?(S)}
   Closed: TYPE = (closed?)    %% = {S: set[T] | closed?(S)}

   IMPORTING reals@intervals_real[T]

   above_intv(a:T)(x) : MACRO bool = x > a
   below_intv(a:T)(x) : MACRO bool = x < a

   a,b: VAR T

%   Open_empty        : LEMMA {x: Open_interval(a,a) | TRUE} = emptyset[T]

   open_intv_open     : LEMMA a < b IMPLIES open?(open_intv(a,b))

   above_intv_open    : LEMMA open?(above_intv(a))
   below_intv_open    : LEMMA open?(below_intv(a))

   union_open         : LEMMA open?(S1) AND open?(S2) IMPLIES
                                 open?(union(S1,S2))

   closed_intv_closed : LEMMA a < b IMPLIES closed?(closed_intv(a,b))

END open_sets

quality91%

¤ 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.11Bemerkung: ¤

*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.