st_mul — Mathlib

English

The standard part is multiplicative on finite hyperreals: st(x·y) = st(x)·st(y).

Русский

Стандартная часть сохраняет умножение для конечных гиперреальных: st(xy) = st(x)st(y).

LaTeX

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

Lean4

theorem st_mul {x y : ℝ*} (hx : ¬Infinite x) (hy : ¬Infinite y) : st (x * y) = st x * st y :=
  have hx' := isSt_st' hx
  have hy' := isSt_st' hy
  have hxy := isSt_st' (not_infinite_mul hx hy)
  hxy.unique (hx'.mul hy')

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