st — Mathlib · SciLib

English

The standard part function st(x) assigns to x its real standard part if one exists, otherwise 0.

Русский

Функция стандартной части st(x) присваивает x его вещественную стандартную часть, если она существует; иначе 0.

LaTeX

$$st(x) = \\begin{cases} r, & \\text{если } \\exists r: \\mathbb{R}, IsSt(x,r), \\\\ 0, & \\text{иначе}. \\end{cases}$$

Lean4

/-- Standard part function: like a "round" to ℝ instead of ℤ -/
noncomputable def st : ℝ* → ℝ := fun x => if h : ∃ r, IsSt x r then Classical.choose h else 0

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