ofReal

Mathlib.Analysis.Real.Hyperreal

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

English

There is a natural embedding of the real numbers into the hyperreals, denoted ofReal.

Русский

Существует естественное вложение чисел в действительных в гиперреальные, обозначаемое as ofReal.

LaTeX

$$$\mathrm{ofReal}: \mathbb{R} \to \mathbb{R}^*$ is the natural embedding.$$

Lean4

/-- Natural embedding `ℝ → ℝ*`. -/
@[coe]
noncomputable def ofReal : ℝ → ℝ* :=
  const

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

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

Разделы

Аффилиация

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