English
The indicators of closed δ-thickenings tend pointwise to the indicator of closure(E) as δ → 0.
Русский
Индикаторы замкнутых δ-уплотнений сходят по точкам к индикатору замыкания(E) при δ → 0.
LaTeX
$$$\\mathrm{Tendsto}\\bigl(\\lambda \\delta. (\\mathrm{Metric.cthickening}_{\\delta} E).\\mathrm{mulIndicator} f\\bigr)\\; (\\mathcal{N}\\;0)\\; (\\mathcal{N}((\\overline{E}).\\mathrm{mulIndicator} f))$$$
Lean4
/-- The multiplicative indicators of closed δ-thickenings of a set tend pointwise to the
multiplicative indicator of the set, as δ tends to zero. -/
@[to_additive /-- The indicators of closed δ-thickenings of a set tend pointwise to the indicator
of the set, as δ tends to zero. -/
]
theorem tendsto_mulIndicator_cthickening_mulIndicator_closure (f : α → β) (E : Set α) :
Tendsto (fun δ ↦ (Metric.cthickening δ E).mulIndicator f) (𝓝 0) (𝓝 ((closure E).mulIndicator f)) :=
by
rw [tendsto_pi_nhds]
intro x
rw [tendsto_congr' (mulIndicator_cthickening_eventually_eq_mulIndicator_closure f E x)]
apply tendsto_const_nhds
