proposition: Lemma filter_finite_indexed_intersection: forall {X:Type} (F:Filter X) {A:Type} (S:IndexedFamily A X), FiniteT A -> (forall a:A, In (filter_family F) (S a)) -> In (filter_family F) (IndexedIntersection S).
proof: Proof. intros. induction H. - rewrite empty_indexed_intersection. apply filter_full. - rewrite IndexedIntersection_option_Intersection. apply filter_intersection. + apply IHFiniteT; auto. + apply H0. - rewrite IndexedIntersection_surj_fn with S f. 2: { apply invertible_impl_bijective in H1. apply H1. } apply IHFiniteT; auto. Qed.
imports: ZornsLemma(DecidableDec FiniteIntersections FunctionProperties)