Theory seq

⊢ ∀f. convergent f ⇔ ∃l. f ⟶ l

⊢ ∀f. lim f = @l. f ⟶ l

⊢ ∀f. mono f ⇔ (∀m n. m ≤ n ⇒ f m ≤ f n) ∨ ∀m n. m ≤ n ⇒ f m ≥ f n

⊢ ∀f. mono_decreasing f ⇔ ∀m n. m ≤ n ⇒ f n ≤ f m

⊢ ∀f. mono_increasing f ⇔ ∀m n. m ≤ n ⇒ f m ≤ f n

⊢ ∀f. subseq f ⇔ ∀m n. m < n ⇒ f m < f n

⊢ ∀f. suminf f = @s. f sums s

⊢ ∀f. summable f ⇔ ∃s. f sums s

⊢ ∀f s. f sums s ⇔ (λn. sum (0,n) f) ⟶ s

⊢ ∀x x0. x ⟶ x0 ⇔ (x tends x0) (mtop mr1,$>=)

⊢ ∀c. c ≤ 0 ⇒ ∀x y. abs x ≤ c * abs y ⇒ (x = 0)

⊢ ∀P. (∀a b c. a ≤ b ∧ b ≤ c ∧ P (a,b) ∧ P (b,c) ⇒ P (a,c)) ∧
      (∀x. ∃d. 0 < d ∧ ∀a b. a ≤ x ∧ x ≤ b ∧ b − a < d ⇒ P (a,b)) ⇒
      ∀a b. a ≤ b ⇒ P (a,b)

⊢ ∀P. (∀a b c. a ≤ b ∧ b ≤ c ∧ P a b ∧ P b c ⇒ P a c) ∧
      (∀x. ∃d. 0 < d ∧ ∀a b. a ≤ x ∧ x ≤ b ∧ b − a < d ⇒ P a b) ⇒
      ∀a b. a ≤ b ⇒ P a b

⊢ ∀x. abs x < 1 ⇒ (λn. x pow n) sums (1 − x)⁻¹

⊢ ∀x. x ≠ 1 ⇒ ∀n. sum (0,n) (λn. x pow n) = (x pow n − 1) / (x − 1)

⊢ summable (λn. (&SUC n)² ⁻¹)

⊢ ∀f l.
    (∀n. f n ≤ f (SUC n)) ∧ (∀n. f n ≤ l) ∧ (∀e. 0 < e ⇒ ∃n. l < f n + e) ⇒
    f ⟶ l

⊢ ∀x y f. (∀n. x ≤ f n) ∧ f ⟶ y ⇒ x ≤ y

⊢ ∀s l. (s ⟶ l) sequentially ⇔ s ⟶ l

⊢ ∀f. lim sequentially f = lim f

⊢ ∀s N. ∃k. ∀n. n < N ⇒ abs (s n) < k

⊢ ∀f. mono f ⇔ (∀n. f (SUC n) ≥ f n) ∨ ∀n. f (SUC n) ≤ f n

⊢ ∀f g.
    (∀n. f (SUC n) ≥ f n) ∧ (∀n. g (SUC n) ≤ g n) ∧ (∀n. f n ≤ g n) ⇒
    ∃l m. l ≤ m ∧ ((∀n. f n ≤ l) ∧ f ⟶ l) ∧ (∀n. m ≤ g n) ∧ g ⟶ m

⊢ ∀f g.
    (∀n. f (SUC n) ≥ f n) ∧ (∀n. g (SUC n) ≤ g n) ∧ (∀n. f n ≤ g n) ∧
    (λn. f n − g n) ⟶ 0 ⇒
    ∃l. ((∀n. f n ≤ l) ∧ f ⟶ l) ∧ (∀n. l ≤ g n) ∧ g ⟶ l

⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃x. ∀n. sum (0,n) f ≤ x) ⇒ summable f

⊢ ∀m n. m ≤ n ⇒ (1 / 2) pow n ≤ (1 / 2) pow m

⊢ (λn. (1 / 2) pow (n + 1)) sums 1

⊢ ∀e. 0 < e ⇒ ∃n. (1 / 2) pow n < e

⊢ ∀x x0. x ⟶ x0 ⇔ ∀e. 0 < e ⇒ ∃N. ∀n. n ≥ N ⇒ abs (x n − x0) < e

⊢ ∀f. (λn. abs (f n)) ⟶ 0 ⇔ f ⟶ 0

⊢ ∀f l. f ⟶ l ⇒ (λn. abs (f n)) ⟶ abs l

⊢ ∀x x0 y y0. x ⟶ x0 ∧ y ⟶ y0 ⇒ (λn. x n + y n) ⟶ (x0 + y0)

⊢ ∀f. bounded (mr1,$>=) f ∧ mono f ⇒ convergent f

⊢ ∀s. bounded (mr1,$>=) s ⇔ ∃k. ∀n. abs (s n) < k

⊢ ∀f k k'. (∀n. k ≤ f n ∧ f n ≤ k') ⇒ bounded (mr1,$>=) f

⊢ ∀f. cauchy f ⇔ convergent f

⊢ ∀f. cauchy f ⇒ bounded (mr1,$>=) f

⊢ ∀k. (λx. k) ⟶ k

⊢ ∀f. subseq f ⇒ ∀N1 N2. ∃n. n ≥ N1 ∧ f n ≥ N2

⊢ ∀x x0 y y0. x ⟶ x0 ∧ y ⟶ y0 ∧ y0 ≠ 0 ⇒ (λn. x n / y n) ⟶ (x0 / y0)

⊢ ∀f. bounded (mr1,$>=) f ∧ (∀m n. m ≥ n ⇒ f m ≥ f n) ⇒ convergent f

⊢ ∀x x0. x ⟶ x0 ∧ x0 ≠ 0 ⇒ (λn. (x n)⁻¹) ⟶ x0⁻¹

⊢ ∀f. (∀y. ∃N. ∀n. n ≥ N ⇒ f n > y) ⇒ (λn. (f n)⁻¹) ⟶ 0

⊢ ∀f g l m. f ⟶ l ∧ g ⟶ m ∧ (∃N. ∀n. n ≥ N ⇒ f n ≤ g n) ⇒ l ≤ m

⊢ ∀x y f. (∀n. f n ≤ x) ∧ f ⟶ y ⇒ y ≤ x

⊢ ∀f x n. (∀n. f (n + 1) ≤ f n) ∧ f ⟶ x ⇒ x ≤ f n

⊢ ∀f. convergent f ⇔ f ⟶ lim f

⊢ ∀s. ∃f. subseq f ∧ mono (λn. s (f n))

⊢ ∀f x n. (∀n. f n ≤ f (n + 1)) ∧ f ⟶ x ⇒ f n ≤ x

⊢ ∀x x0 y y0. x ⟶ x0 ∧ y ⟶ y0 ⇒ (λn. x n * y n) ⟶ (x0 * y0)

⊢ ∀x x0. x ⟶ x0 ⇔ (λn. -x n) ⟶ -x0

⊢ ∀f. bounded (mr1,$>=) (λn. -f n) ⇔ bounded (mr1,$>=) f

⊢ ∀f. convergent f ⇔ convergent (λn. -f n)

⊢ ∀c. abs c < 1 ⇒ (λn. c pow n) ⟶ 0

⊢ ∀c. abs c < 1 ⇒ (λn. abs c pow n) ⟶ 0

⊢ ∀s. FINITE s ⇒
      ∀f f'.
        (∀x. x ∈ s ⇒ (λn. f n x) ⟶ f' x) ⇒ (λn. SIGMA (f n) s) ⟶ SIGMA f' s

⊢ ∀f g h l. f ⟶ l ∧ h ⟶ l ∧ (∀n. f n ≤ g n ∧ g n ≤ h n) ⇒ g ⟶ l

⊢ ∀s f. bounded (mr1,$>=) s ⇒ bounded (mr1,$>=) (λn. s (f n))

⊢ ∀x x0 y y0. x ⟶ x0 ∧ y ⟶ y0 ⇒ (λn. x n − y n) ⟶ (x0 − y0)

⊢ ∀f. subseq f ⇒ ∀n. n ≤ f n

⊢ ∀f l. f ⟶ l ⇔ (λn. f (SUC n)) ⟶ l

⊢ ∀x x1 x2. x ⟶ x1 ∧ x ⟶ x2 ⇒ (x1 = x2)

⊢ ∀f n. (∀m. n ≤ m ⇒ (f m = 0)) ⇒ f sums sum (0,n) f

⊢ ∀f. summable (λn. abs (f n)) ⇒ abs (suminf f) ≤ suminf (λn. abs (f n))

⊢ ∀f. summable (λn. abs (f n)) ⇒ summable f

⊢ ∀x x0 y y0. x sums x0 ∧ y sums y0 ⇒ (λn. x n + y n) sums (x0 + y0)

⊢ ∀f. summable f ⇔ ∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ⇒ abs (sum (m,n) f) < e

⊢ ∀x x0 c. x sums x0 ⇒ (λn. x n / c) sums (x0 / c)

⊢ ∀x x0 c. x sums x0 ⇒ (λn. c * x n) sums (c * x0)

⊢ ∀f g. (∃N. ∀n. n ≥ N ⇒ abs (f n) ≤ g n) ∧ summable g ⇒ summable f

⊢ ∀f g.
    (∃N. ∀n. n ≥ N ⇒ abs (f n) ≤ g n) ∧ summable g ⇒
    summable (λk. abs (f k))

⊢ ∀f k. summable f ∧ 0 < k ⇒ (λn. sum (n * k,k) f) sums suminf f

⊢ ∀f g. (∀n. f n ≤ g n) ∧ summable f ∧ summable g ⇒ suminf f ≤ suminf g

⊢ ∀f g.
    (∀n. abs (f n) ≤ g n) ∧ summable g ⇒ summable f ∧ suminf f ≤ suminf g

⊢ ∀x x0. x sums x0 ⇒ (λn. -x n) sums -x0

⊢ ∀f. summable f ⇒ ∀k. (λn. f (n + k)) sums (suminf f − sum (0,k) f)

⊢ ∀f. summable f ⇒ (λn. sum (2 * n,2) f) sums suminf f

⊢ ∀f. summable f ∧ (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f

⊢ ∀f g.
    (∀n. 0 ≤ f n) ∧ summable g ∧ (∀n. f n ≤ g n) ⇒
    summable f ∧ suminf f ≤ suminf g

⊢ ∀f n. summable f ∧ (∀m. n ≤ m ⇒ 0 ≤ f m) ⇒ sum (0,n) f ≤ suminf f

⊢ ∀f n. summable f ∧ (∀m. n ≤ m ⇒ 0 < f m) ⇒ sum (0,n) f < suminf f

⊢ ∀f n.
    summable f ∧ (∀d. 0 < f (n + 2 * d) + f (n + (2 * d + 1))) ⇒
    sum (0,n) f < suminf f

⊢ ∀f. (∀n. 0 ≤ f n) ⇒ mono (λn. sum (0,n) f)

⊢ ∀f c N.
    c < 1 ∧ (∀n. n ≥ N ⇒ abs (f (SUC n)) ≤ c * abs (f n)) ⇒ summable f

⊢ ∀x x0 y y0. x sums x0 ∧ y sums y0 ⇒ (λn. x n − y n) sums (x0 − y0)

⊢ ∀f. summable f ⇒ f ⟶ 0

⊢ ∀f. subseq f ⇔ ∀n. f n < f (SUC n)

⊢ ∀f g h.
    (∀m n. 0 ≤ f m n) ∧ (∀n. f n sums g n) ∧ summable g ∧
    BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    UNCURRY f ∘ h sums suminf g

⊢ ∀f g.
    summable f ∧ summable g ⇒
    summable (λn. f n + g n) ∧
    (suminf f + suminf g = suminf (λn. f n + g n))

⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ 0 ≤ suminf f

⊢ ∀f x. summable f ∧ (∀n. sum (0,n) f ≤ x) ⇒ suminf f ≤ x

⊢ ∀f. summable f ⇒ f sums suminf f

⊢ ∀f x. f sums x ⇔ summable f ∧ (suminf f = x)

⊢ K 0 sums 0

⊢ ∀n r. sum (0,n) (K r) = &n * r

⊢ ∀f l. f sums l ⇒ summable f

⊢ ∀f x. f sums x ⇒ (x = suminf f)

⊢ ∀f. cauchy f ⇔ ∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ∧ n ≥ N ⇒ abs (f m − f n) < e

⊢ ∀f. mono_decreasing f ⇔ ∀n. f (SUC n) ≤ f n

⊢ ∀f r. mono_increasing f ∧ f ⟶ r ⇒ (r = sup (IMAGE f 𝕌(:num)))

⊢ ∀f. mono_increasing f ⇔ ∀n. f n ≤ f (SUC n)

⊢ ∀f. infsum 𝕌(:num) f = suminf f

⊢ ∀f. real_topology$summable 𝕌(:num) f ⇔ summable f

⊢ ∀f l. real_topology$sums f l 𝕌(:num) ⇔ f sums l