Commit 2023-10-29 04:04 a988ad93

feat: a unique cluster pt of a filter is its limit (#7944) If a filter has a unique cluster point in a compact set, then this point is a limit of the filter. We add four versions of this fact:

• for a compact set or a compact space;
• for a ClusterPt and _ ≤ 𝓝 _ or MapClusterPt and Filter.Tendsto _ _ (𝓝 _). Also
• add isCompact_iff_ultrafilter_le_nhds' that uses s ∈ f instead of ↑f ≤ 𝓟 s;
• move Ultrafilter.le_nhds_lim to a more appropriate file. Motivated by a lemma in the Mandelbrot set connectedness project. Co-Authored-By: @girving