English
Let f: α → β and E ⊆ α. Then for every x ∈ α, as δ > 0 tends to 0 from the right, the multiplicative indicator of the δ-thickening of E at x coincides with the multiplicative indicator of the closure of E at x, eventually.
Русский
Пусть f: α → β и E ⊆ α. Тогда для каждой точки x ∈ α, при δ > 0, стремящемся к нулю справа, точечный мультипликативный индикатор δ-уплотнения E в x совпадает с индикатором замыкания E в x, когда δ достаточно мало.
LaTeX
$$$\\forall x, \\forall^\\!_{\\delta \\to 0^+} (\\mathrm{thickening}_\\delta E).\\mathrm{mulIndicator} f\,x = (\\overline{E}).\\mathrm{mulIndicator} f\,x$$$
Lean4
/-- Pointwise, the multiplicative indicators of δ-thickenings of a set eventually coincide
with the multiplicative indicator of the set as δ>0 tends to zero. -/
@[to_additive /-- Pointwise, the indicators of δ-thickenings of a set eventually coincide
with the indicator of the set as δ>0 tends to zero. -/
]
theorem mulIndicator_thickening_eventually_eq_mulIndicator_closure (f : α → β) (E : Set α) (x : α) :
∀ᶠ δ in 𝓝[>] (0 : ℝ), (Metric.thickening δ E).mulIndicator f x = (closure E).mulIndicator f x :=
by
by_cases x_mem_closure : x ∈ closure E
· filter_upwards [self_mem_nhdsWithin] with δ δ_pos
simp only [closure_subset_thickening δ_pos E x_mem_closure, mulIndicator_of_mem, x_mem_closure]
· have obs := eventually_notMem_thickening_of_infEdist_pos x_mem_closure
filter_upwards [mem_nhdsWithin_of_mem_nhds obs, self_mem_nhdsWithin] with δ x_notin_thE _
simp only [x_notin_thE, not_false_eq_true, mulIndicator_of_notMem, x_mem_closure]
