English
A simplified version: under T1-space, the Tendsto of indicator constants to A is equivalent to Tendsto to the pi-pure product.
Русский
Условия T1 пространства дают эквивалентность: предел индикаторных констант к A эквивалентен пределам к произведению чистых функция.
LaTeX
$$$\text{Tendsto} (i \mapsto (A_i).indicator(\cdot)) L \mathcal{N}(A.indicator(\cdot)) \iff \text{Tendsto } A L (\operatorname{pi} (\text{pure} \circ \in A))$$$
Lean4
theorem tendsto_indicator_const_iff_tendsto_pi_pure [T1Space β] (b : β) [NeZero b] :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b))) ↔
(Tendsto As L <| Filter.pi (pure <| · ∈ A)) :=
by
rw [tendsto_indicator_const_iff_forall_eventually _ b, tendsto_pi]
simp_rw [tendsto_pure]
aesop