proposition: Lemma connectedPn A : ~ connected A <-> exists E : bool -> set T, [/\ forall b, E b !=set0, A = E false `|` E true & separated (E false) (E true)].
proof: Proof. rewrite -propeqE; apply: notLR; rewrite propeqE. split=> [conE [E [E0 EU [E1 E2]]]|conE B B0 [C oC BAC] [D cD BAD]]. suff : E true = A. move/esym/(congr1 (setD^~ (closure (E true)))); rewrite EU setDUl. have := @subset_closure _ (E true); rewrite -setD_eq0 => ->; rewrite setU0. by move/setDidPl : E2 => ->; exact/eqP/set0P. apply: (conE _ (E0 true)). - exists (~` (closure (E false))); first exact/closed_openC/closed_closure. rewrite EU setIUl. have /subsets_disjoint -> := @subset_closure _ (E false); rewrite set0U. by apply/esym/setIidPl/disjoints_subset; rewrite setIC. - exists (closure (E true)); first exact: closed_closure. by rewrite EU setIUl E2 set0U; exact/esym/setIidPl/subset_closure. apply: contrapT => AF; apply: conE. exists (fun i => if i is false then A `\` C else A `&` C); split. - case=> /=; first by rewrite -BAC. apply/set0P/eqP => /disjoints_subset; rewrite setCK => EC. by apply: AF; rewrite BAC; exact/setIidPl. - by rewrite setDE -setIUr setUCl setIT. - split. + rewrite setIC; apply/disjoints_subset; rewrite closureC => x [? ?]. by exists C => //; split=> //; rewrite setDE setCI setCK; right. + apply/disjoints_subset => y -[Ay Cy]. rewrite -BAC BAD => /closureI[_]; move/closure_id : cD => <- Dy. by have : B y; [by rewrite BAD; split|rewrite BAC => -[]]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed