proposition: Lemma finite_intersections_Im_inverse_image {X Y : Type} (f : Y -> X) (F : Family X) (U : Ensemble X) : In (finite_intersections F) U -> In (finite_intersections (Im F (inverse_image f))) (inverse_image f U).
proof: Proof. intros H. induction H. - rewrite inverse_image_full. constructor. - apply FiniteIntersections.intro_S. apply Im_def. assumption. - rewrite inverse_image_intersection. apply FiniteIntersections.intro_intersection; auto. Qed.
imports: Coq(ClassicalChoice Lia Program.Equality) ZornsLemma(EnsemblesImplicit InverseImage Proj1SigInjective)