Theorems · Theorem · functional analysis

NormedRing.inverse_add_norm

∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ),
  (fun t => Ring.inverse (↑x + t)) =O[nhds 0] fun _t => 1

The function fun t ↦ inverse (x + t) is O(1) as t → 0.

Defined in

Mathlib.Analysis.Normed.Ring.Units

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedRingHasSummableGeomSeries