English
For any x, st x equals sSup of reals below x; if x is infinite, the equality relates to special cases.
Русский
Для любого x стандартная часть x равна sSup множества действительных чисел, меньших x; в бесконечном случае аналогично.
LaTeX
$$$\\forall x:\\\\mathbb{R}^*, \\ st(x) = sSup\\{ y : \\\\mathbb{R} \\mid (y : \\\\mathbb{R}^*) < x \\}$$$
Lean4
theorem st_eq_sSup {x : ℝ*} : st x = sSup {y : ℝ | (y : ℝ*) < x} :=
by
rcases _root_.em (Infinite x) with (hx | hx)
· rw [hx.st_eq]
cases hx with
| inl hx =>
convert Real.sSup_univ.symm
exact Set.eq_univ_of_forall hx
| inr hx =>
convert Real.sSup_empty.symm
exact Set.eq_empty_of_forall_notMem fun y hy ↦ hy.out.not_gt (hx _)
· exact (isSt_sSup hx).st_eq
