Theorems · Theorem · functional analysis

controlled_sum_of_mem_closure_range

∀ {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] {j : E →+ F}
  {b : F},
  b ∈ closure ↑j.range →
    ∀ {f : ℕ → ℝ},
      (∀ (n : ℕ), 0 < f n) →
        ∃ a,
          Filter.Tendsto (fun n => ∑ i ∈ Finset.range (n + 1), j (a i)) Filter.atTop (nhds b) ∧
            ‖-j (a 0) + b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Defined in

Mathlib.Analysis.Normed.Group.Continuity

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup