proposition: Lemma surj_finite: forall (X Y:Type) (f:X->Y), FiniteT X -> surjective f -> (forall y1 y2:Y, y1=y2 \/ y1<>y2) -> FiniteT Y.
proof: Proof. intros. apply bij_finite with {y:Y | In (Im Full_set f) y} (@proj1_sig _ (fun y:Y => In (Im Full_set f) y)). apply Finite_ens_type. apply FiniteT_img. assumption. assumption. assert (forall y:Y, In (Im Full_set f) y). intro. destruct (H0 y). exists x; auto with sets. constructor. pose (proj1_sig_inv := fun y:Y => exist (fun y0:Y => In (Im Full_set f) y0) y (H2 y)). exists proj1_sig_inv. destruct x. simpl. unfold proj1_sig_inv. destruct (proof_irrelevance _ (H2 x) i); trivial. intros; simpl; reflexivity. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description