| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle non_empty_bounded_sets.pvs Sprache: PVS |
|||||||||
|
% non-empty sets of reals that are bounded from above or below.
% These are exactly the sets that have least upper (greatest lower) bounds. % % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Dec 2004 % % non_empty_finite_bounded_above and non_empty_finite_bounded_below added % 13 Jan 2005 by Jerry James (james@acm.org), University of Kansas non_empty_bounded_sets[T: TYPE FROM real]: THEORY BEGIN IMPORTING total_lattices[T, <=] non_empty_bounded_above?(S: set[T]): bool = nonempty?[T](S) & bounded_above?[T](<=)(S) non_empty_bounded_below?(S: set[T]): bool = nonempty?[T](S) & bounded_below?[T](<=)(S) non_empty_bounded_above_is_nonempty: JUDGEMENT (non_empty_bounded_above?) SUBTYPE_OF (nonempty?[T]) non_empty_bounded_above_is_bounded_above: JUDGEMENT (non_empty_bounded_above?) SUBTYPE_OF (bounded_above?[T](<=)) non_empty_bounded_below_is_nonempty: JUDGEMENT (non_empty_bounded_below?) SUBTYPE_OF (nonempty?[T]) non_empty_bounded_below_is_bounded_below: JUDGEMENT (non_empty_bounded_below?) SUBTYPE_OF (bounded_below?[T](<=)) non_empty_finite_bounded_above: JUDGEMENT non_empty_finite_set[T] SUBTYPE_OF (non_empty_bounded_above?) non_empty_finite_bounded_below: JUDGEMENT non_empty_finite_set[T] SUBTYPE_OF (non_empty_bounded_below?) END non_empty_bounded_sets ¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28