% 2/2014 % Summary: If a function f:T1->T2 is surjective, % if t has k elements, and the preimage of t % has a fixed number d of elements for every t % in T2, then T1 has k*d elements and there is a % bijection T1 -> T2 x below(d). This is actually % proved on subsets of T1 and T2 instead of the % full types.
BEGIN
S1 : VAR set[T1]
S2 : VAR set[T2]
k,d : VAR posnat
finite_index: LEMMA FORALL (f:[(S1)->(S2)]):
(EXISTS (b1:[(S2)->below(k)]): bijective?(b1)) AND
(FORALL (s2:(S2)): LET PI = inverse_image(f,singleton(s2)) IN EXISTS (b2:[(PI)->below(d)]): bijective?(b2)) IMPLIES
((EXISTS (b:[(S1)->[(S2),below(d)]]): bijective?(b)) AND
(EXISTS (b:[(S1)->below(k*d)]): bijective?(b)))
END index_theorems
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
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.
