infinitePos_iff_infinite_and_pos

Mathlib.Analysis.Real.Hyperreal

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

← MathLib Explorer

English

If x is InfinitePos, then not Infinitesimal x.

Русский

Если x бесконечно велико положительно, то x не бесконечно мало.

LaTeX

$$$InfinitePos\ x \Rightarrow \neg Infinitesimal(x)$$$

Lean4

theorem infinitePos_iff_infinite_and_pos {x : ℝ*} : InfinitePos x ↔ Infinite x ∧ 0 < x :=
  ⟨fun hip => ⟨Or.inl hip, hip 0⟩, fun ⟨hi, hp⟩ => hi.casesOn id fun hin => False.elim (not_lt_of_gt hp (hin 0))⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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