exists_st_iff_not_infinite

Mathlib.Analysis.Real.Hyperreal

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

English

There exists a standard part iff x is not infinite.

Русский

Существование стандартной части эквивалентно тому, что x не бесконечно велико.

LaTeX

$$$(\\\\exists r: \\\\mathbb{R}, IsSt(x,r)) \\iff \\\\neg Infinite x$$$

Lean4

theorem exists_st_iff_not_infinite {x : ℝ*} : (∃ r : ℝ, IsSt x r) ↔ ¬Infinite x :=
  ⟨not_infinite_of_exists_st, exists_st_of_not_infinite⟩

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

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

Разделы

Аффилиация

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