infinite_neg

Mathlib.Analysis.Real.Hyperreal

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem infinite_neg {x : ℝ*} : Infinite (-x) ↔ Infinite x :=
  or_comm.trans <| infiniteNeg_neg.or infinitePos_neg

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

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

Разделы

Аффилиация

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