infiniteNeg_add_not_infinite — Mathlib

English

Let x, y be hyperreal numbers. If x is infinitely negative and y is finite, then x+y is infinitely negative.

Русский

Пусть x — гиперреальное число, у которого бесконечно малая отрицательная часть, а y — конечное число. Тогда сумма x+y бесконечно отрицательна.

LaTeX

$$$\\forall x,y \\in \\mathbb{R}^*,\\ InfiniteNeg(x) \\land \\neg Infinite(y) \\rightarrow InfiniteNeg(x+y)$$$

Lean4

theorem infiniteNeg_add_not_infinite {x y : ℝ*} : InfiniteNeg x → ¬Infinite y → InfiniteNeg (x + y) := fun hx hy =>
  infiniteNeg_add_not_infinitePos hx (not_or.mp hy).1

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