infinitesimal_neg

Mathlib.Analysis.Real.Hyperreal

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

English

Infinitesimal(-x) if and only if Infinitesimal(x).

Русский

Infinitesimal(-x) тогда и только тогда, когда Infinitesimal(x).

LaTeX

$$$\\forall {x : \\mathbb{R}^*}, Infinitesimal(-x) \\iff Infinitesimal(x)$$$

Lean4

@[simp]
theorem infinitesimal_neg {x : ℝ*} : Infinitesimal (-x) ↔ Infinitesimal x :=
  ⟨fun h => neg_neg x ▸ h.neg, Infinitesimal.neg⟩

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

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

Разделы

Аффилиация

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