inverse_add_norm_diff_first_order

English

For a unit x, the map t ↦ inverse( x + t) − x⁻¹ is O(‖t‖) as t → 0.

Русский

Для единицы x отображение t ↦ (x+t)⁻¹ − x⁻¹ имеет порядок O(‖t‖) при t → 0.

LaTeX

$$$\left( t \mapsto (x+t)^{-1} - x^{-1} \right) = O\left(\|t\|\right) \text{ as } t \to 0$$$

Lean4

/-- The function `fun t ↦ Ring.inverse (x + t) - x⁻¹` is `O(t)` as `t → 0`. -/
theorem inverse_add_norm_diff_first_order (x : Rˣ) : (fun t : R => inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ := by
  simpa using inverse_add_norm_diff_nth_order x 1

Похожие утверждения