infinitePos_iff_infinite_of_pos

Mathlib.Analysis.Real.Hyperreal

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

English

If x ≥ 0, then InfinitePos x iff Infinite x.

Русский

Если x ≥ 0, то InfinitePos x ⇔ Infinite x.

LaTeX

$$$0 \le x \Rightarrow InfinitePos x \iff Infinite x$$$

Lean4

theorem infinitePos_iff_infinite_of_pos {x : ℝ*} (hp : 0 < x) : InfinitePos x ↔ Infinite x :=
  infinitePos_iff_infinite_of_nonneg hp.le

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

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

Разделы

Аффилиация

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