%------------------------------------------------------------------------------ % Hausdorff 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 %------------------------------------------------------------------------------
hausdorff_convergence[T:TYPE,(IMPORTING topology_def[T]) S:hausdorff]: THEORY
BEGIN
IMPORTING topological_convergence[T,S]
u: VAR sequence[T]
v: VAR convergent
x,l,l1,l2: VAR T
unique_limit: LEMMA convergence?(u,l1) AND convergence?(u,l2) => l1 = l2
limit_def: LEMMA limit(v) = l IFF convergence?(v, l)
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.
