| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 6 kB |
|
Quellcode-Bibliothek topological_convergence.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Topological convergence % % Author: David Lester, Manchester University, NIA, Université Perpignan % % All references are to WA Sutherland "Introduction to Metric and % Topological Spaces", OUP, 1981 % % Version 1.0 06/09/06 Initial Version %------------------------------------------------------------------------------ topological_convergence[T:TYPE,(IMPORTING topology_def[T]) S:topology[T]]: THEORY BEGIN IMPORTING topology[T,S], sequences[T], reals@real_fun_preds[nat], subseq[T] U: VAR open u,u1,u2: VAR sequence l: VAR T a: VAR T i,n: VAR nat convergence?(u,l):bool = FORALL U: U(l) => EXISTS n: FORALL i: i >= n => U(u(i)) accumulation?(u, a): bool = FORALL U,n: U(a) => EXISTS i: i >= n AND U(u(i)) convergent?(u): bool = EXISTS l: convergence?(u, l) tconvergent?(u): MACRO bool = convergent?(u) convergent: TYPE = (convergent?) v : VAR convergent limit(v):T = epsilon(LAMBDA l: convergence?(v, l)) limit_lemma : LEMMA convergence?(v, limit(v)) limit_accumulation : LEMMA convergence?(u, l) => accumulation?(u, l) convergence_subsequence : LEMMA convergence?(u1, l) AND subseq?(u2, u1) => convergence?(u2, l) END topological_convergence ¤ 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.12Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
