infinitesimal_iff_infinite_inv

Mathlib.Analysis.Real.Hyperreal

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

← MathLib Explorer

English

For x ≠ 0, Infinitesimal x iff Infinite x⁻¹.

Русский

Для x ≠ 0: Infinitesimal x эквивален Infinite x⁻¹.

LaTeX

$$$ x \neq 0 \Rightarrow (\operatorname{Infinitesimal}(x) \iff \operatorname{Infinite}(x^{-1})) $$$

Lean4

theorem infinitesimal_iff_infinite_inv {x : ℝ*} (h : x ≠ 0) : Infinitesimal x ↔ Infinite x⁻¹ :=
  Iff.trans (by rw [inv_inv]) (infinite_iff_infinitesimal_inv (inv_ne_zero h)).symm

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

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

Разделы

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

Аффилиация

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