proposition: Lemma compact_closed (A : set T) : hausdorff_space -> compact A -> closed A.
proof: Proof. move=> hT Aco p clAp; have pA := !! @withinT _ (nbhs p) A _. have [q [Aq clsAp_q]] := !! Aco _ _ pA; rewrite (hT p q) //. by apply: cvg_cluster clsAp_q; apply: cvg_within. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed