English
If f sends the complement of s to a single point x, then f tends to x along l restricted to s iff it tends to x along l.
Русский
Если функция f отправляет дополнение к s в одну точку x, то стремление f к x по l ограничено множеством s эквивалентно стремлению по l без ограничений.
LaTeX
$$Tendsto f (l \\cap 𝓟 s) (𝓝 x) \\iff Tendsto f l (𝓝 x) \\quad\\text{under } (∀ a \\notin s, f a = x)$$
Lean4
/-- Suppose that `f` sends the complement to `s` to a single point `x`, and `l` is some filter.
Then `f` tends to `x` along `l` restricted to `s` if and only if it tends to `x` along `l`. -/
theorem tendsto_inf_principal_nhds_iff_of_forall_eq {f : α → X} {l : Filter α} {s : Set α} (h : ∀ a ∉ s, f a = x) :
Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x) :=
by
rw [tendsto_iff_comap, tendsto_iff_comap]
replace h : 𝓟 sᶜ ≤ comap f (𝓝 x) := by
rintro U ⟨t, ht, htU⟩ x hx
have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
exact htU this
refine ⟨fun h' => ?_, le_trans inf_le_left⟩
have := sup_le h' h
rw [sup_inf_right, sup_principal, union_compl_self, principal_univ, inf_top_eq, sup_le_iff] at this
exact this.1
