Commit 2024-10-08 06:33 f082d6ee

chore: more coherent lemma names between nhds and nhdsWithin (#17432) Currently, we have lemmas eventually_eventually_nhds and eventually_nhdsWithin_nhdsWithin, which correspond to each other. Rename the latter to eventually_eventually_nhdsWithin for coherence. Also, we have eventually_mem_nhds and eventually_mem_nhdsWithin, which have completely different contents. To lift the bad correspondence, rename eventually_mem_nhds to eventually_mem_nhds_iff, and add a corresponding lemma eventually_mem_nhdsWithin_iff.