infinitePos_add_not_infinite — 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 infinitePos_add_not_infinite {x y : ℝ*} : InfinitePos x → ¬Infinite y → InfinitePos (x + y) := fun hx hy =>
  infinitePos_add_not_infiniteNeg hx (not_or.mp hy).2

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