infiniteNeg_mul_infiniteNeg — Mathlib

English

If x and y are infinite-negative hyperreal numbers, then their product xy is infinite-positive.

Русский

Пусть x и y — бесконечно отрицательные гиперреальные числа; их произведение xy бесконечно велико и положительно.

LaTeX

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

Lean4

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

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