Theorems · Theorem · real analysis

IsCauSeq.of_abv_le

∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [IsAbsoluteValue abv] {f : ℕ → β} {a : ℕ → α} (n : ℕ),
  (∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m) →
    (IsCauSeq abs fun n => ∑ i ∈ Finset.range n, a i) → IsCauSeq abv fun n => ∑ i ∈ Finset.range n, f i

Defined in

Mathlib.Algebra.Order.CauSeq.BigOperators

Cited by

2 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRingRingIsAbsoluteValue