English
For each x, the Tendsto of the i-th indicator value equals the indicator of A at x if and only if eventually x ∈ As(i) ↔ x ∈ A.
Русский
Для каждого x предел значения индикатора равен индикатору A в x тогда и только тогда, когда в большинстве i выполняется x ∈ As(i) ↔ x ∈ A.
LaTeX
$$$\forall x,\; \operatorname{Tendsto}\big(i \mapsto (\mathbf{1}_{A_i}(x)\cdot b)\big)\;L\; (\mathbf{1}_{A}(x)\cdot b) \ \Longleftrightarrow\ \forall^\infty i\, (x \in A_i \iff x \in A)$$$
Lean4
theorem tendsto_indicator_const_apply_iff_eventually' (b : β) (nhds_b : {0}ᶜ ∈ 𝓝 b) (nhds_o : { b }ᶜ ∈ 𝓝 0) (x : α) :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b) x) L (𝓝 (A.indicator (fun (_ : α) ↦ b) x)) ↔
∀ᶠ i in L, (x ∈ As i ↔ x ∈ A) :=
by
classical
have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β)) nhds_o nhds_b ?_ ?_
· convert heart
by_cases hxA : x ∈ A <;> simp [hxA]
· simp only [principal_singleton, le_def, mem_pure]
exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
· simp only [principal_singleton, le_def, mem_pure]
exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
