English
Equivalent formulation: Tendsto indicator constants to A is equivalent to Tendsto of As to the PI-pure product.
Русский
Эквивалентная формулировка: предел индикаторных функций эквивалентен пределам As к произведению чистых на каждом входе.
LaTeX
$$$\operatorname{tendsto\_indicator\_const\_iff\_tendsto\_pi\_pure' (L) (A) (b)$$$
Lean4
theorem tendsto_indicator_const_iff_tendsto_pi_pure' (b : β) (nhds_b : {0}ᶜ ∈ 𝓝 b) (nhds_o : { b }ᶜ ∈ 𝓝 0) :
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 nhds_b nhds_o, tendsto_pi]
simp_rw [tendsto_pure]
aesop