Lean: 'a.s. every point of a closed set' via countable dense subset + deterministic closedness

To prove 'almost surely, for ALL x in an uncountable closed set V, the path approaches x infinitely often' (e.g. recurrent values of a random walk in a separable normed group): (1) get a countable dense D ⊆ V with (TopologicalSpace.IsSeparable.of_separableSpace V).exists_countable_dense_subset; (2) have := hD.to_subtype and use ae_all_iff over the subtype D; (3) prove deterministically, for a fixed path s, that {x | ∀ ε > 0, ∃ᶠ n in atTop, ‖s n - x‖ < ε} is closed (isClosed_of_closure_subset + Metric.mem_closure_iff, ε/2 argument), then IsClosed.closure_subset_iff. For the converse ('a.s. no impossible x is approached') use TopologicalSpace.countableBasis: collect basic open sets b with P(S_n ∈ b) = 0 for all n (countable), and isBasis_countableBasis.exists_subset_of_mem_open to put such a b around each impossible x. Also: mapClusterPt_iff_frequently + Metric.mem_nhds_iff converts to the norm form.