|
index_theorems[T1:Type,T2:Type]: THEORY
% 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.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
