proposition: Lemma accessible_finite_set_closed : accessible_space <-> forall A : set T, finite_set A -> closed A.
proof: Proof. split => [TT1 A fA|h x y xy]. rewrite -(fsbig_setU_set1 fA) fsbig_finite//=. by apply: closed_bigsetU => x xA; exact: accessible_closed_set1. exists (~` [set y]); split; first by rewrite openC; exact: h. by rewrite !inE/=; split=> [|/eqP]; [exact/eqP|rewrite eqxx]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed