infiniteNeg_add_not_infinitePos — 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_not_infinitePos {x y : ℝ*} : InfiniteNeg x → ¬InfinitePos y → InfiniteNeg (x + y) :=
  by
  rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]
  exact infinitePos_add_not_infiniteNeg

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