proposition: Lemma connected_union: forall {X:TopologicalSpace} {A:Type} (S:IndexedFamily A X), (forall a:A, connected (SubspaceTopology (S a))) -> Inhabited (IndexedIntersection S) -> IndexedUnion S = Full_set -> connected X.
proof: Proof. intros. pose (inc := fun (a:A) => subspace_inc (S a)). destruct H0, H0. red; intros. assert (forall a:A, clopen (inverse_image (inc a) S0)). { intro. apply continuous_clopen; auto. apply subspace_inc_continuous. } destruct (classic (In S0 x)). - right. assert (forall a:A, inverse_image (inc a) S0 = Full_set). { intro. destruct (H a _ (H3 a)). - assert (In (@Empty_set (SubspaceTopology (S a))) (exist _ x (H0 a))). { rewrite <- H5. now constructor. } now destruct H6. - assumption. } extensionality_ensembles. + constructor. + assert (In (IndexedUnion S) x0). { rewrite H1. constructor. } destruct H6. assert (In (@Full_set (SubspaceTopology (S a))) (exist _ x0 H6)) by constructor. rewrite <- H5 in H7. now destruct H7. - left. assert (forall a:A, inverse_image (inc a) S0 = Empty_set). { intros. destruct (H a _ (H3 a)). - assumption. - assert (In (@Full_set (SubspaceTopology (S a))) (exist _ x (H0 a))) by constructor. rewrite <- H5 in H6. destruct H6. contradiction H4. } extensionality_ensembles. assert (In (IndexedUnion S) x0). { rewrite H1. constructor. } destruct H7. assert (In (@Empty_set (SubspaceTopology (S a))) (exist _ x0 H7)). { rewrite <- H5. now constructor. } destruct H8. Qed.
imports: TopologicalSpaces Homeomorphisms SubspaceTopology ZornsLemma(EnsemblesTactics Powerset_facts)