proposition: Lemma connected_closure A : connected A -> connected (closure A).
proof: Proof. move=> ctdA U U0 [C1 oC1 C1E] [C2 cC2 C2E]; rewrite eqEsubset C2E; split => //. suff : A `<=` U. move/closure_subset; rewrite [_ `&` _](iffLR (closure_id _)) ?C2E//. by apply: closedI => //; exact: closed_closure. rewrite -setIidPl; apply: ctdA. - move: U0; rewrite C1E => -[z [clAx C1z]]; have [] := clAx C1. exact: open_nbhs_nbhs. by move=> w [Aw C1w]; exists w; rewrite setIA (setIidl (@subset_closure _ _)). - by exists C1 => //; rewrite C1E setIA (setIidl (@subset_closure _ _)). - by exists C2 => //; rewrite C2E setIA (setIidl (@subset_closure _ _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed