st_id_real

Mathlib.Analysis.Real.Hyperreal

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

English

The standard part of a real number equals the number itself: st(r) = r for r ∈ ℝ.

Русский

Стандартная часть вещественного числа равна самому числу: st(r) = r для r ∈ ℝ.

LaTeX

$$$\forall r \in \mathbb{R}, \ \mathrm{st}(r) = r$$$

Lean4

theorem st_id_real (r : ℝ) : st r = r :=
  (isSt_refl_real r).st_eq

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

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

Разделы

Аффилиация

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