infinitePos_abs_iff_infinite

Mathlib.Analysis.Real.Hyperreal

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

English

InfinitePos |x| is equivalent to Infinite |x|.

Русский

InfinitePos |x| эквивалентно Infinite |x|.

LaTeX

$$$InfinitePos(|x|) \iff Infinite(|x|)$$$

Lean4

@[simp]
theorem infinitePos_abs_iff_infinite {x : ℝ*} : InfinitePos |x| ↔ Infinite x :=
  infinitePos_abs_iff_infinite_abs.trans infinite_abs_iff

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

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

Разделы

Аффилиация

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