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
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|