st_inv — Mathlib

English

If x is not Infinite, then x − st(x) is infinitesimal.

Русский

Если x не бесконечно велико, то x − st(x) инфинитезимальна.

LaTeX

$$$\neg \operatorname{Infinite}(x) \Rightarrow \operatorname{Infinitesimal}(x - \operatorname{st}(x))$$$

Lean4

theorem st_inv (x : ℝ*) : st x⁻¹ = (st x)⁻¹ := by
  by_cases h0 : x = 0
  · rw [h0, inv_zero, ← coe_zero, st_id_real, inv_zero]
  by_cases h1 : Infinitesimal x
  · rw [((infinitesimal_iff_infinite_inv h0).mp h1).st_eq, h1.st_eq, inv_zero]
  by_cases h2 : Infinite x
  · rw [(infinitesimal_inv_of_infinite h2).st_eq, h2.st_eq, inv_zero]
  exact ((isSt_st' h2).inv h1).st_eq

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