coe_ne_one

Mathlib.Analysis.Real.Hyperreal

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

English

For every real x, the hyperreal image is not equal to 1 if and only if x is not equal to 1.

Русский

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

LaTeX

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

Lean4

@[norm_cast]
theorem coe_ne_one {x : ℝ} : (x : ℝ*) ≠ 1 ↔ x ≠ 1 :=
  coe_ne_coe

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

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

Разделы

Аффилиация

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