coe_eq_one

Mathlib.Analysis.Real.Hyperreal

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

English

For every real x, the hyperreal image of x equals 1 if and only if x equals 1.

Русский

Для каждого вещественного числа x гиперреальная образующая x равна 1 тогда и только тогда, когда x = 1.

LaTeX

$$$\\forall x \\\in \\mathbb{R}, \\ x^{\\*} = 1 \\iff x = 1$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_one {x : ℝ} : (x : ℝ*) = 1 ↔ x = 1 :=
  coe_eq_coe

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

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

Разделы

Аффилиация

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