not_infinite_add — Mathlib

English

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

Русский

Пусть x и y конечны; тогда x+y конечен.

LaTeX

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

Lean4

theorem not_infinite_add {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
  not_infinite_of_exists_st <| ⟨r + s, hr.add hs⟩

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