tendsto_indicator_const_iff_forall_eventually'

English

The indicator functions converge pointwise if and only if for every x, eventually x ∈ As(i) ↔ x ∈ A.

Русский

Индикаторные функции сходятся по точкам тогда и только тогда, когда для каждого x в большинстве i выполняется x ∈ As(i) ↔ x ∈ A.

LaTeX

$$$\forall x, \forall^\infty i \,(x \in A_i \iff x \in A)$$$

Lean4

theorem tendsto_indicator_const_iff_forall_eventually' (b : β) (nhds_b : {0}ᶜ ∈ 𝓝 b) (nhds_o : { b }ᶜ ∈ 𝓝 0) :
    Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b))) ↔
      ∀ x, ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A) :=
  by
  simp_rw [tendsto_pi_nhds]
  apply forall_congr'
  exact tendsto_indicator_const_apply_iff_eventually' L b nhds_b nhds_o

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