Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/Gnome/po/   (Gnome Linux Desktop Version 4.23.2©)  Datei vom 30.5.2026 mit Größe 242 kB image not shown  

Bilddatei

topological_convergence.pvs


products/Sources/formale Sprachen/PVS/topology/topological_convergence.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