infinitePos_abs_iff_infinite_abs

Mathlib.Analysis.Real.Hyperreal

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

English

Infinite(-x) is equivalent to Infinite(x).

Русский

Infinite(-x) эквивалентно Infinite(x).

LaTeX

$$$Infinite(-x) \iff Infinite(x)$$$

Lean4

theorem infinitePos_abs_iff_infinite_abs {x : ℝ*} : InfinitePos |x| ↔ Infinite |x| :=
  infinitePos_iff_infinite_of_nonneg (abs_nonneg _)

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

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

Разделы

Аффилиация

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