| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/metric_space/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 553 B |
|
Quelle test_cont.pvsSprache: 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 am 2026-06-15) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09