English
The kernel of the neighborhood filter at x equals the set of all y that specialize to x.
Русский
Ядро фильтра окрестностей в x равно множеству y, которые специализируются на x.
LaTeX
$$$ (\mathcal{N}(x)).\ker = \{ y\mid y \!\;⤳\; x\}$$$
Lean4
/-- The indicator functions of `Asᵢ` evaluated at `x` tend to the indicator function of `A`
evaluated at `x` if and only if we eventually have the equivalence `x ∈ Asᵢ ↔ x ∈ A`. -/
@[simp]
theorem tendsto_indicator_const_apply_iff_eventually [T1Space β] (b : β) [NeZero b] (x : α) :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b) x) L (𝓝 (A.indicator (fun (_ : α) ↦ b) x)) ↔
∀ᶠ i in L, (x ∈ As i ↔ x ∈ A) :=
by
apply tendsto_indicator_const_apply_iff_eventually' _ b
· simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]
· simp only [compl_singleton_mem_nhds_iff, ne_eq, (NeZero.ne b).symm, not_false_eq_true]
