Theorems · Theorem · sequences and series

AbsoluteValue.tendsto_div_one_add_pow_nhds_zero

∀ {R : Type u_2} {S : Type u_3} [inst : Field R] [inst_1 : Field S] [inst_2 : LinearOrder S]
  [inst_3 : TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [_i : OrderTopology S] {v : AbsoluteValue R S}
  {a : R}, 1 < v a → Filter.Tendsto (fun n => v (1 / (1 + a ^ n))) Filter.atTop (nhds 0)

v (1 / (1 + a ^n)) tends to 0 whenever v : AbsoluteValue R S for fields R and S, provided 1 < v a.

Defined in

Mathlib.Analysis.SpecificLimits.Normed

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldLinearOrderTopologicalSpaceIsStrictOrderedRingArchimedeanOrderTopology