proposition: Lemma clopen_connectedP : connected A <-> (forall U, @clopen [the topologicalType of subspace A] U -> U `<=` A -> U !=set0 -> U = A).
proof: Proof. split. move=> + U [/open_subspaceP oU /closed_subspaceP cU] UA U0; apply => //. - case: oU => V [oV VAUA]; exists V; rewrite // setIC VAUA. exact/esym/setIidPl. - case: cU => V [cV VAUA]; exists V => //; rewrite setIC VAUA. exact/esym/setIidPl. move=> clpnA U Un0 [V oV UVA] [W cW UWA]; apply: clpnA => //; first split. - by apply/open_subspaceP; exists V; rewrite setIC UVA setIAC setIid. - by apply/closed_subspaceP; exists W; rewrite setIC UWA setIAC setIid. - by rewrite UWA; exact: subIsetl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed