|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
