|
%------------------------------------------------------------------------------
% Continuity
%
% All references are to:
%
% WA Sutherland "Introduction to Metric and Topological Spaces", OUP, 1981
%
% or
%
% TM Apostol "Mathematical Analysis" 2nd ed, Addison-Wesley, 1974
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 5/12/04 Initial Version
% Version 1.1 9/6/06 Changed Interface
%------------------------------------------------------------------------------
continuity[T1:Type, (IMPORTING topology_def[T1]) S:topology[T1],
T2:Type, (IMPORTING topology_def[T2]) T:topology[T2]]: THEORY
BEGIN
IMPORTING continuity_def[T1,S,T2,T],
topology[T1,S],
topology[T2,T],
basis[T2]
X: VAR set[T1]
Y: VAR set[T2]
f: VAR [T1->T2]
% Apostol Theorem 4.23
continuous_open_sets: THEOREM
continuous?(f) IFF
(FORALL Y: open?[T2,T](Y) => open?[T1,S](inverse_image(f,Y)))
% Apostol Theorem 4.24
continuous_closed_sets: THEOREM
continuous?(f) IFF
(FORALL Y: closed?[T2,T](Y) => closed?[T1,S](inverse_image(f,Y)))
B: VAR (base?[T2](T))
continuous_basis: THEOREM
continuous?(f) IFF FORALL (Y:(B)): open?[T1,S](inverse_image(f,Y))
END continuity
¤ Dauer der Verarbeitung: 0.1 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.
|
