tsum_coe_eq_top_iff_not_summable_coe

English

If all f(i) ≠ ∞ and x ≠ ∞, then Tendsto toReal of f is equivalent to Tendsto f to x.

Русский

Если все f(i) ≠ ∞ и x ≠ ∞, тогда Tendsto(f(i).toReal) равно Tendsto(f(i)) к x.

LaTeX

$$$\\forall i, f(i) \\neq \\infty \\Rightarrow (Tendsto (\\lambda n. (f n).toReal) f (nhds x.toReal) \\iff Tendsto f f (nhds x))$$$

Lean4

theorem tsum_coe_eq_top_iff_not_summable_coe {f : α → ℝ≥0} : (∑' a, (f a : ℝ≥0∞)) = ∞ ↔ ¬Summable fun a => (f a : ℝ) :=
  tsum_coe_ne_top_iff_summable_coe.not_right

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