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