proposition: Lemma bigcup_connected I (A : I -> set T) (P : I -> Prop) : \bigcap_(i in P) (A i) !=set0 -> (forall i, P i -> connected (A i)) -> connected (\bigcup_(i in P) (A i)).
proof: Proof. move=> [c AIc] cA; have [[i Pi]|] := pselect (exists i, P i); last first. move/forallNP => P0. rewrite (_ : P = set0) ?bigcup_set0; first exact: connected0. by rewrite predeqE => x; split => //; exact: P0. apply/connectedP => [E [E0 EU sE]]. wlog E0c : E E0 EU sE / E false c. move=> G; have : (\bigcup_(i in P) A i) c by exists i => //; exact: AIc. rewrite EU => -[E0c|E1c]; first exact: G. by apply: (G (E \o negb)) => //; [case => /=|rewrite EU setUC|rewrite separatedC]. move: (E0 true) => /set0P/eqP; apply. have [/eqP //|/set0P[d E1d]] := boolP (E true == set0). have : \bigcup_(i in P) A i `<=` E false. suff AE : forall i, P i -> A i `<=` E false by move=> x [j ? ?]; exact: (AE j). move=> j Pj. move: (@connected_subset _ _ (A j) sE). rewrite -EU => /(_ (bigcup_sup _) (cA _ Pj)) [//| | AjE1]; first exact. exfalso; have E1c := AjE1 _ (AIc _ Pj). by move/separated_disjoint : sE; apply/eqP/set0P; exists c. rewrite EU subUset => -[_] /(_ _ E1d) E0d; exfalso. by move/separated_disjoint : sE; apply/eqP/set0P; exists d. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed