proposition: Lemma finite_indexed_intersection_is_finite_intersection: forall {X:Type} (S:Family X) (J:Type) (V:J->Ensemble X), FiniteT J -> (forall j:J, In S (V j)) -> In (finite_intersections S) (IndexedIntersection V).
proof: Proof. intros. induction H. - rewrite empty_indexed_intersection. constructor. - rewrite IndexedIntersection_option_Intersection. constructor 3; auto. constructor 2; trivial. - rewrite IndexedIntersection_surj_fn with V f. 2: { apply invertible_impl_bijective in H1. destruct H1. assumption. } apply IHFiniteT. auto. Qed.
imports: Coq(ClassicalChoice Lia Program.Equality) ZornsLemma(EnsemblesImplicit InverseImage Proj1SigInjective)