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.0 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|