not_infinite_of_exists_st

Mathlib.Analysis.Real.Hyperreal

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

English

If there exists r with IsSt x r, then x is not infinite.

Русский

Если существует r, такое что IsSt(x,r), то x не бесконечно велико.

LaTeX

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

Lean4

theorem not_infinite_of_exists_st {x : ℝ*} : (∃ r : ℝ, IsSt x r) → ¬Infinite x := fun ⟨_r, hr⟩ => hr.not_infinite

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

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

Разделы

Аффилиация

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