tendsto_indicator_const_iff_tendsto_pi_pure'

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

Похожие утверждения