Theorems · Theorem · functional analysis

controlled_prod_of_mem_closure_range

∀ {E : Type u_4} {F : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup 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

SeminormedCommGroupSeminormedCommGroup