English
The Tendsto of indicator constants to A is equivalent to Tendsto of the index family to the pi-product of pure memberships.
Русский
Сходимость индикаторных констант к A эквивалентна сходимости семейства индексов к произведению по чистым принадлежностям.
LaTeX
$$$\operatorname{Tendsto}\big(i \mapsto (A_i).indicator(\cdot)\big) L \mathcal{N}(A.indicator(\cdot)) \iff \operatorname{Tendsto} A L (\operatorname{pi} (\text{pure} \circ \in A))$$$
Lean4
/-- The indicator functions of `Asᵢ` tend to the indicator function of `A` pointwise if and only if
for every `x`, we eventually have the equivalence `x ∈ Asᵢ ↔ x ∈ A`. -/
@[simp]
theorem tendsto_indicator_const_iff_forall_eventually [T1Space β] (b : β) [NeZero b] :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b))) ↔
∀ x, ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A) :=
by
apply tendsto_indicator_const_iff_forall_eventually' _ b
· simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]
· simp only [compl_singleton_mem_nhds_iff, ne_eq, (NeZero.ne b).symm, not_false_eq_true]
