Theorems · Theorem · functional analysis

controlled_prod_of_mem_closure

∀ {E : Type u_4} [inst : SeminormedCommGroup E] {a : E} {s : Subgroup 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

1 results in Mathlib

Foundations

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

Assumes

SeminormedCommGroup