Commit 2023-10-30 03:09 65ab68cb

feat: ∃ᶠ x in 𝓝 a, x < a (#7941)

• Add frequently_lt_nhds and frequently_gt_nhds.
• Move some lemmas from Topology/Order/Basic to Topology/Algebra/Order/LeftRight.
• Relax TC assumptions in Filter.Eventually.exists_lt (and *_gt). New versions assume NeBot (𝓝[<] a) and NeBot (𝓝[>] a), so the latter one can be applied, e.g., to ((a : ℝ≥0) : ℝ≥0∞). From the Mandelbrot set connectedness project. Co-Authored-By: @girving