From bb85b99d2844823177a228409a402c2631e45bd8 Mon Sep 17 00:00:00 2001 From: Anatole Dedecker Date: Wed, 31 Jan 2024 10:21:13 +0000 Subject: [PATCH] feat: fix typo (eventually_nhds_subtype_if -> eventually_nhds_subtype_iff) (#10124) This was unnoticed during the review of #7568 --- Mathlib/Topology/ContinuousOn.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index 39f45c51ce88a..afade60dcc8a6 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -505,13 +505,13 @@ theorem preimage_coe_mem_nhds_subtype {s t : Set α} {a : s} : (↑) ⁻¹' t rw [← map_nhds_subtype_val, mem_map] #align preimage_coe_mem_nhds_subtype preimage_coe_mem_nhds_subtype -theorem eventually_nhds_subtype_if (s : Set α) (a : s) (P : α → Prop) : +theorem eventually_nhds_subtype_iff (s : Set α) (a : s) (P : α → Prop) : (∀ᶠ x : s in 𝓝 a, P x) ↔ ∀ᶠ x in 𝓝[s] a, P x := preimage_coe_mem_nhds_subtype theorem frequently_nhds_subtype_iff (s : Set α) (a : s) (P : α → Prop) : (∃ᶠ x : s in 𝓝 a, P x) ↔ ∃ᶠ x in 𝓝[s] a, P x := - eventually_nhds_subtype_if s a (¬ P ·) |>.not + eventually_nhds_subtype_iff s a (¬ P ·) |>.not theorem tendsto_nhdsWithin_iff_subtype {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) : Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l := by