infinitePos_iff_infinite_of_nonneg

Mathlib.Analysis.Real.Hyperreal

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

English

For x, InfinitePos x is equivalent to Infinite x and x > 0.

Русский

Для x: InfinitePos x ⇔ Infinite x и x > 0.

LaTeX

$$$InfinitePos x \leftrightarrow Infinite x \land 0 < x$$$

Lean4

theorem infinitePos_iff_infinite_of_nonneg {x : ℝ*} (hp : 0 ≤ x) : InfinitePos x ↔ Infinite x :=
  .symm <| or_iff_left fun h ↦ h.lt_zero.not_ge hp

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

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

Разделы

Аффилиация

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