gt_of_neg_of_infinitesimal

Mathlib.Analysis.Real.Hyperreal

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

← MathLib Explorer

English

If x is infinitesimal and r < 0, then r < x.

Русский

Если x бесконечно мал и r < 0, то r < x.

LaTeX

$$$\\forall {x : \\mathbb{R}^*}, \\ Infinitesimal(x) \\rightarrow \\forall r \\in \\mathbb{R}, r < 0 \\rightarrow (r : \\mathbb{R}^*) < x$$$

Lean4

theorem gt_of_neg_of_infinitesimal {x : ℝ*} (hi : Infinitesimal x) (r : ℝ) (hr : r < 0) : ↑r < x :=
  neg_neg r ▸ (infinitesimal_def.1 hi (-r) (neg_pos.2 hr)).1

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

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

Разделы

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

Аффилиация

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