Theorems · Theorem · sequences and series

AbsoluteValue.tendsto_div_one_add_pow_nhds_one

∀ {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}, v a < 1 → Filter.Tendsto (fun n => v (1 / (1 + a ^ n))) Filter.atTop (nhds 1)

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

Defined in

Mathlib.Analysis.SpecificLimits.Normed

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldLinearOrderTopologicalSpaceIsStrictOrderedRingArchimedeanOrderTopology