isSt_st

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.IsSt.isSt_st

English

If x is infinitesimally close to r, then x is infinitesimally close to st x.

Русский

Если x бесконечно близко к r, то x бесконечно близко к st(x).

LaTeX

$$IsSt x r → IsSt x (st x)$$

Lean4

theorem isSt_st {x : ℝ*} {r : ℝ} (hxr : IsSt x r) : IsSt x (st x) := by rwa [hxr.st_eq]

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

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

Разделы

Аффилиация

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