infinite_iff_not_exists_st

Mathlib.Analysis.Real.Hyperreal

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

English

An equivalent form: x is infinite iff there is no r with IsSt x r.

Русский

Бесконечно велико тогда и только тогда, когда не существует r с IsSt(x,r).

LaTeX

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

Lean4

theorem infinite_iff_not_exists_st {x : ℝ*} : Infinite x ↔ ¬∃ r : ℝ, IsSt x r :=
  iff_not_comm.mp exists_st_iff_not_infinite

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

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

Разделы

Аффилиация

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