proposition: Lemma component_closed A x : closed A -> closed (connected_component A x).
proof: Proof. move=> clA; have [Ax|Ax] := pselect (A x); first last. by rewrite connected_component_out //; exact: closed0. rewrite closure_id eqEsubset; split; first exact: subset_closure. move=> z Axz; exists (closure (connected_component A x)) => //. split; first exact/subset_closure/connected_component_refl. rewrite [X in _ `<=` X](closure_id A).1//. by apply: closure_subset; exact: connected_component_sub. by apply: connected_closure; exact: component_connected. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed