feat(topology/continuous_on): generalise lemma slightly (#16840)

Generalise `frequently_nhds_within_iff` to allow `within` any set, not just complement of singleton



Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>

Author: b-mehta

src/topology/continuous_on.lean

@@ -44,9 +44,9 @@ lemma eventually_nhds_within_iff {a : α} {s : set α} {p : α → Prop} :
   (∀ᶠ x in 𝓝[s] a, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x :=
 eventually_inf_principal
 
-lemma frequently_nhds_within_iff {z : α} {p : α → Prop} :
-  (∃ᶠ x in 𝓝[≠] z, p x) ↔ (∃ᶠ x in 𝓝 z, p x ∧ x ≠ z) :=
-iff.not (by simp [eventually_nhds_within_iff, not_imp_not])
+lemma frequently_nhds_within_iff {z : α} {s : set α} {p : α → Prop} :
+  (∃ᶠ x in 𝓝[s] z, p x) ↔ (∃ᶠ x in 𝓝 z, p x ∧ x ∈ s) :=
+iff.not (by simp [eventually_nhds_within_iff, not_and'])
 
 lemma mem_closure_ne_iff_frequently_within {z : α} {s : set α} :
   z ∈ closure (s \ {z}) ↔ ∃ᶠ x in 𝓝[≠] z, x ∈ s :=