Quelle  test_cont.pvs   Sprache: unbekannt

%
% 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

quality96%

[ zur Elbe Produktseite wechseln0.4Quellennavigators  Analyse erneut starten  ]