isSt_st' — Mathlib

English

If x is a finite hyperreal, then x is standard with respect to its standard part, i.e., IsSt x (st x).

Русский

Если x является конечным гиперреалом, то он является стандартным по отношению к своей стандартной части st(x).

LaTeX

$$$\neg \mathrm{Infinite}(x) \Rightarrow \mathrm{IsSt}(x, \mathrm{st}(x))$$$

Lean4

theorem isSt_st' {x : ℝ*} (hx : ¬Infinite x) : IsSt x (st x) :=
  (isSt_sSup hx).isSt_st

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