infinitePos_mul_infinitePos — Mathlib

English

If x and y are infinite-positive hyperreal numbers, then their product xy is also infinite-positive. The collection of infinite-positive hyperreals is closed under multiplication.

Русский

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

LaTeX

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

Lean4

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

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