infiniteNeg_add_infiniteNeg — Mathlib

English

Sum of two infinitely negative hyperreals is infinitely negative.

Русский

Сумма двух бесконечно отрицательных гиперреальных чисел бесконечно отрицательна.

LaTeX

$$$InfiniteNeg x \land InfiniteNeg y \Rightarrow InfiniteNeg(x + y)$$$

Lean4

theorem infiniteNeg_add_infiniteNeg {x y : ℝ*} : InfiniteNeg x → InfiniteNeg y → InfiniteNeg (x + y) := fun hx hy =>
  infiniteNeg_add_not_infinitePos hx hy.not_infinitePos

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