|
%------------------------------------------------------------------------------
% Subspace Continuity
%
% Continuity is preserved on subspaces
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 8/10/04 Initial Version
% Version 1.1 9/06/06 Changed interface, added Type Judgements
%------------------------------------------------------------------------------
continuity_subspace[T1:TYPE, (IMPORTING topology_def[T1]) S:topology[T1],
T2:TYPE, (IMPORTING topology_def[T2]) T:topology[T2],
T3:TYPE FROM T1]: THEORY
BEGIN
IMPORTING subspace[T1,S,T3],
continuity[T1,S,T2,T],
continuity
x: VAR T3
f: VAR [T1->T2]
subspace_continuous_at: LEMMA continuous_at?(f,x) =>
continuous_at?[T3,induced_topology,T2,T](restrict[T1,T3,T2](f),x)
subspace_continuous: LEMMA continuous?(f) =>
continuous?[T3,induced_topology,T2,T](restrict[T1,T3,T2](f))
F: VAR continuous[T1,S,T2,T]
restrict_is_continuous:
JUDGEMENT restrict[T1,T3,T2](F) HAS_TYPE
continuous[T3,induced_topology,T2,T]
END continuity_subspace
¤ 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.
|
