|
%------------------------------------------------------------------------------
% Complex Topology
%
% Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Version 1.0 12/3/10 Initial Version
%------------------------------------------------------------------------------
complex_topology: THEORY
BEGIN
IMPORTING complex_alt@polar,
metric_space@metric_space[complex,lambda (x,y:complex): abs(x-y)]
a,x,y: VAR complex
r: VAR posreal
q: VAR {x | rational?(Re(x)) & rational?(Im(x))}
pq: VAR posrat
X,A: VAR set[complex]
IMPORTING metric_space@real_topology % Proof Only
complex_is_complete: JUDGEMENT fullset[complex] HAS_TYPE
metric_complete[complex,lambda x,y: abs(x-y)]
END complex_topology
¤ Dauer der Verarbeitung: 0.13 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.
|
