proposition: Lemma inverse_image_finite {X Y : Type} (f : X -> Y) (F : Family X) : surjective f -> Finite _ F -> Finite _ (inverse_image (inverse_image f) F).
proof: Proof. intros Hf H. induction H. - rewrite inverse_image_empty_set. constructor. - unfold Add. rewrite inverse_image_union2. pose proof (Singleton_is_finite _ (Im x f)). now eapply Union_preserves_Finite, Finite_downward_closed, inverse_image_surjective_singleton. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies