ne_zero

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.Infinite.ne_zero

English

If x is Infinite, then x ≠ 0.

Русский

Если x бесконечен, то x ≠ 0.

LaTeX

$$$\forall {x} \; \mathrm{Infinite}(x) \Rightarrow x \neq 0$$$

Lean4

theorem ne_zero {x : ℝ*} (hI : Infinite x) : x ≠ 0 :=
  hI.elim (fun hip => hip.pos.ne') fun hin => hin.lt_zero.ne

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

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

Разделы

Аффилиация

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