| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/metric_space/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 553 B |
|
Quelle test_cont.pvs Sprache: PVS |
|||||||||
|
%
% 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.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28