Theorems · Theorem · commutative algebra

tendsto_seminormFromConst_seq_atTop

∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 →
    f c ≠ 0 →
      IsPowMul ⇑f →
        ∀ (x : R), Filter.Tendsto (seminormFromConst_seq c f x) Filter.atTop (nhds (seminormFromConst' c f x))

We prove that seminormFromConst' c f x is the limit of the sequence seminormFromConst_seq c f x as n tends to infinity.

Defined in

Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommRing