|
%
% Although this doesn't look right (1/x is continuous?), it is correct,
% provided that the domain is taken to be the metric induced topology
% restricted to the nonzero reals.
%
% This is a test that continuity_subspace captures the desired property.
% (And it does!)
test_cont: THEORY
BEGIN
IMPORTING real_topology,
continuity_subspace[real,(LAMBDA (x,y:real): abs(x-y)),
real,(LAMBDA (x,y:real): abs(x-y)),nzreal]
recip_continuous: LEMMA metric_continuous?(lambda (x:nzreal): 1/x)
END test_cont
¤ Dauer der Verarbeitung: 0.28 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.
|
