| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 561 B |
|
Quelle reals_complete_more.pvs Sprache: PVS |
|||||||||
|
reals_complete_more[T: TYPE FROM real]: THEORY
BEGIN IMPORTING bound_defs[real,T] real_complete2: LEMMA % this could replace real_complete in prelude (FORALL (S: (nonempty?[T])): (EXISTS (y: real): upper_bound(<=)(y, S)) IMPLIES (EXISTS (x: real): least_upper_bound(<=)(x, S))) real_lower_complete2: LEMMA % this could replace real_complete in prelude (FORALL (S: (nonempty?[T])): (EXISTS (y : real): lower_bound(<=)(y, S)) IMPLIES (EXISTS (x: real): greatest_lower_bound(<=)(x, S))) END reals_complete_more ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28