English
Let f: α → β and E ⊆ α. Then for every x ∈ α, as δ → 0 (in the usual real topology), the multiplicative indicator of the closed δ-thickening of E at x converges to the multiplicative indicator of the closure of E at x.
Русский
Пусть f: α → β и E ⊆ α. Тогда для каждой точки x ∈ α, при δ → 0, индикатором замкнутого δ-уплотнения E в x сходится к индикатору замыкания E в x.
LaTeX
$$$\\forall x, \\forall^\\!_{\\delta \\to 0} (\\mathrm{Metric.cthickening}_{\\delta} E).\\mathrm{mulIndicator} f\\,x = (\\overline{E}).\\mathrm{mulIndicator} f\\,x$$$
Lean4
/-- Pointwise, the multiplicative indicators of closed δ-thickenings of a set eventually coincide
with the multiplicative indicator of the set as δ tends to zero. -/
@[to_additive /-- Pointwise, the indicators of closed δ-thickenings of a set eventually coincide
with the indicator of the set as δ tends to zero. -/
]
theorem mulIndicator_cthickening_eventually_eq_mulIndicator_closure (f : α → β) (E : Set α) (x : α) :
∀ᶠ δ in 𝓝 (0 : ℝ), (Metric.cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x :=
by
by_cases x_mem_closure : x ∈ closure E
· filter_upwards [univ_mem] with δ _
have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]
· filter_upwards [eventually_notMem_cthickening_of_infEdist_pos x_mem_closure] with δ hδ
simp only [hδ, not_false_eq_true, mulIndicator_of_notMem, x_mem_closure]
