proposition: Lemma countable_img {X Y : Type} (f : X -> Y) (S : Ensemble X) : Countable S -> Countable (Im S f).
proof: Proof. intros. assert (forall x, In S x -> In (Im S f) (f x)) by auto with sets. pose (fS := fun x => match x with | exist x0 i => exist _ (f x0) (H0 x0 i) end). apply surj_countable with fS; trivial. intros [? [x i y e]]. exists (exist _ x i). simpl. generalize (H0 x i); intro. generalize (Im_intro X Y S f x i y e); intro. now apply subset_eq. Qed.
imports: Coq(Arith ArithRing ClassicalChoice Description FunctionalExtensionality Lia Relation_Definitions Program.Subset QArith ZArith) ZornsLemma(CSB DecidableDec DependentTypeChoice Finite_sets FiniteTypes FunctionPropertiesEns IndexedFamilies InfiniteTypes)