Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
finite_sets_aux.pvs
Sprache: PVS
|
finite_sets_aux[T: TYPE+]: THEORY
BEGIN
N: VAR nat
is_finite_exists_N: LEMMA FORALL (g: [below[N] -> T]):
is_finite({r: T | EXISTS (n: below[N]): r = g(n)})
END finite_sets_aux
[ zur Elbe Produktseite wechseln0.17Quellennavigators
Analyse erneut starten
]
|
|
