infinite_iff_abs_lt_abs

Mathlib.Analysis.Real.Hyperreal

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

← MathLib Explorer

English

For x, Infinite x iff for every real r, |r| < |x|.

Русский

Для x: Infinite x ⇔ для всех действительных r выполняется |r| < |x|.

LaTeX

$$$Infinite x \iff \forall r \in \mathbb{R}, |r| < |x|$$$

Lean4

theorem infinite_iff_abs_lt_abs {x : ℝ*} : Infinite x ↔ ∀ r : ℝ, (|r| : ℝ*) < |x| :=
  infinitePos_abs_iff_infinite.symm.trans ⟨fun hI r => coe_abs r ▸ hI |r|, fun hR r => (le_abs_self _).trans_lt (hR r)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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