isSt_st_of_exists_st

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.isSt_st_of_exists_st

English

If there exists r with IsSt x r, then IsSt x at its standard part.

Русский

Если существует r с IsSt(x,r), то IsSt x уst(x).

LaTeX

$$IsSt x (st x)$$

Lean4

theorem isSt_st_of_exists_st {x : ℝ*} (hx : ∃ r : ℝ, IsSt x r) : IsSt x (st x) :=
  let ⟨_r, hr⟩ := hx;
  hr.isSt_st

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru