proposition: Lemma subspace_cvgP (F : set_system T) (x : T) : Filter F -> A x -> (F --> (x : subspace A)) <-> (F --> within A (nbhs x)).
proof: Proof. by case: _ / nbhs_subspaceP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed