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