Theorems · Theorem · functional analysis

controlled_sum_of_mem_closure

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

Defined in

Mathlib.Analysis.Normed.Group.Continuity

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroup