infinitePos_add_not_infiniteNeg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem infinitePos_add_not_infiniteNeg {x y : ℝ*} : InfinitePos x → ¬InfiniteNeg y → InfinitePos (x + y) :=
  by
  intro hip hnin r
  obtain ⟨r₂, hr₂⟩ := not_forall.mp hnin
  convert add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂) using 1
  simp

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