infinitePos_mul_infiniteNeg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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