st_add — Mathlib

English

If x and y are finite, then st(x+y) = st(x) + st(y).

Русский

Если x и y конечны, то стандартная часть суммы равна сумме стандартных частей.

LaTeX

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

Lean4

theorem st_add {x y : ℝ*} (hx : ¬Infinite x) (hy : ¬Infinite y) : st (x + y) = st x + st y :=
  (isSt_st' (not_infinite_add hx hy)).unique ((isSt_st' hx).add (isSt_st' hy))

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