tendsto_indicator_const_iff_tendsto_pi_pure

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

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