not_infinite_mul — Mathlib

English

If x and y are finite, then x·y is finite.

Русский

Если x и y конечны, то x·y конечен.

LaTeX

$$$\\forall x,y:\\mathbb{R}^*, \\neg Infinite(x) \\land \\neg Infinite(y) \\rightarrow \\neg Infinite(x \\cdot y)$$$

Lean4

theorem not_infinite_mul {x y : ℝ*} (hx : ¬Infinite x) (hy : ¬Infinite y) : ¬Infinite (x * y) :=
  have ⟨_r, hr⟩ := exists_st_of_not_infinite hx
  have ⟨_s, hs⟩ := exists_st_of_not_infinite hy
  (hr.mul hs).not_infinite

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