infinitesimal_sub_st

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.infinitesimal_sub_st

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 infinitesimal_sub_st {x : ℝ*} (hx : ¬Infinite x) : Infinitesimal (x - ↑(st x)) :=
  (isSt_st' hx).infinitesimal_sub

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru