isSt_ofSeq_iff_tendsto — Mathlib

English

For any f: N → R and r ∈ R, IsSt(ofSeq f) r is equivalent to Tendsto f to r along the hypernatural filter.

Русский

Для любой последовательности f: N → R и действительного числа r, IsSt(ofSeq f) r эквивалентно стремлению f к r вдоль гипернатурального фильтра.

LaTeX

$$$IsSt(\\\\ofSeq f) r \\\\iff Tendsto f (hyperfilter\\\\ Nat) (nhds r)$$$

Lean4

theorem isSt_ofSeq_iff_tendsto {f : ℕ → ℝ} {r : ℝ} : IsSt (ofSeq f) r ↔ Tendsto f (hyperfilter ℕ) (𝓝 r) :=
  Iff.trans (forall₂_congr fun _ _ ↦ (ofSeq_lt_ofSeq.and ofSeq_lt_ofSeq).trans eventually_and.symm)
    (nhds_basis_Ioo_pos _).tendsto_right_iff.symm

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