st_eq

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.Infinite.st_eq

English

If x is infinite, then its standard part is 0.

Русский

Если x бесконечно велико, то его стандартная часть равна нулю.

LaTeX

$$$Infinite x \\Rightarrow st x = 0$$$

Lean4

theorem st_eq {x : ℝ*} (hi : Infinite x) : st x = 0 :=
  dif_neg fun ⟨_r, hr⟩ ↦ hr.not_infinite hi

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

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

Разделы

Аффилиация

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