not_infiniteNeg_add_infinitePos — Mathlib

English

If not InfiniteNeg x and InfinitePos y, then InfinitePos (x + y).

Русский

Если x не бесконечно отрицательно и y бесконечно велико положительно, то x + y бесконечно велико положительно.

LaTeX

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

Lean4

theorem not_infiniteNeg_add_infinitePos {x y : ℝ*} : ¬InfiniteNeg x → InfinitePos y → InfinitePos (x + y) :=
  fun hx hy => add_comm y x ▸ infinitePos_add_not_infiniteNeg hy hx

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