mem_notConvergentSeq_iff — Mathlib

English

Characterizes membership in notConvergentSeq by a quantified existence of a threshold and index after which the edist bound holds.

Русский

Характеризует членство в notConvergentSeq через существование порога и индекса, после которого выполняется неравенство edist.

LaTeX

$$$x\in notConvergentSeq(f,g,n,j) \iff \exists k \ge j, (n)^{-1} < edist(f_k(x), g(x))$$$

Lean4

theorem mem_notConvergentSeq_iff [Preorder ι] {x : α} :
    x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, (n : ℝ≥0∞)⁻¹ < edist (f k x) (g x) := by
  simp_rw [notConvergentSeq, Set.mem_iUnion, exists_prop, mem_setOf]

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