infinitesimal_sub — Mathlib

English

If an element x is infinitely close to a real number r, then the difference x − r is infinitesimal.

Русский

Если x бесконечно близко к действительному r, то разность x − r инфинитезимальна.

LaTeX

$$$ \IsSt(x, r) \Rightarrow \operatorname{Infinitesimal}(x - r) $$$

Lean4

theorem infinitesimal_sub {x : ℝ*} {r : ℝ} (hxr : IsSt x r) : Infinitesimal (x - ↑r) := by
  simpa only [sub_self] using hxr.sub (isSt_refl_real r)

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