infiniteNeg_mul_infinitePos — Mathlib

English

If x is infinite-negative and y is infinite-positive, then their product is infinite-negative.

Русский

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

LaTeX

$$$\mathrm{InfiniteNeg}(x) \land \mathrm{InfinitePos}(y) \Rightarrow \mathrm{InfiniteNeg}(xy)$$$

Lean4

theorem infiniteNeg_mul_infinitePos {x y : ℝ*} : InfiniteNeg x → InfinitePos y → InfiniteNeg (x * y) := fun hx hy =>
  infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hx hy.not_infinitesimal (hy 0)

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