IsSt

Mathlib.Analysis.Real.Hyperreal

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

English

Standard part predicate: IsSt(x, r) holds exactly when x lies infinitesimally close to r.

Русский

Предикат стандартной части: IsSt(x, r) означает, что x бесконечно близко к r.

LaTeX

$$$IsSt(x,r) \iff \\forall \\delta>0, \\\\;(r-\\\\delta) < x \\\\land x < (r+\\\\delta)$$$

Lean4

/-- Standard part predicate -/
def IsSt (x : ℝ*) (r : ℝ) :=
  ∀ δ : ℝ, 0 < δ → (r - δ : ℝ*) < x ∧ x < r + δ

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

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

Разделы

Аффилиация

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