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. assert (IndexedIntersection V = Intersection (IndexedIntersection (fun j:T => V (Some j))) (V None)). apply Extensionality_Ensembles; split; red; intros. destruct H1. constructor. constructor. trivial. trivial. destruct H1. constructor. destruct H1. destruct a as [j|]; trivial. rewrite H1. constructor 3; auto. constructor 2; trivial. destruct H1 as [g]. assert (IndexedIntersection V = IndexedIntersection (fun x:X0 => V (f x))). apply Extensionality_Ensembles; split; red; intros. destruct H3. constructor. trivial. destruct H3. constructor. intro. rewrite <- (H2 a). trivial. rewrite H3; auto. Qed.
imports: Coq(Program.Equality) Coq(Lia) Coq(ClassicalChoice) Ensembles EnsemblesImplicit Families FiniteTypes IndexedFamilies CountableTypes Proj1SigInjective Powerset_facts