English
If x is infinite and y is not infinitesimal, then xy is infinite.
Русский
Если x бесконечно велико, а y не бесконечно малое (не бесконечно малое), то xy бесконечно велико.
LaTeX
$$$\mathrm{Infinite}(x) \land \lnot \mathrm{Infinitesimal}(y) \Rightarrow \mathrm{Infinite}(xy)$$$
Lean4
theorem infinite_mul_of_infinite_not_infinitesimal {x y : ℝ*} : Infinite x → ¬Infinitesimal y → Infinite (x * y) :=
fun hx hy =>
have h0 : y < 0 ∨ 0 < y := lt_or_gt_of_ne fun H0 => hy (Eq.substr H0 (isSt_refl_real 0))
hx.elim
(h0.elim (fun H0 Hx => Or.inr (infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg Hx hy H0)) fun H0 Hx =>
Or.inl (infinitePos_mul_of_infinitePos_not_infinitesimal_pos Hx hy H0))
(h0.elim (fun H0 Hx => Or.inl (infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg Hx hy H0)) fun H0 Hx =>
Or.inr (infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos Hx hy H0))
