coe_toNNReal

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.coe_toNNReal

English

For every i in the unit interval, the real-valued projection of toNNReal(i) equals i itself, i.e., the underlying real equals the interval value.

Русский

Для каждого i из единичного интервала вещественная величина toNNReal(i) совпадает с i.

LaTeX

$$$((toNNReal x) : \\mathbb{R}) = x \\quad (x\\in I)$$$

Lean4

@[simp]
theorem coe_toNNReal (x : I) : ((toNNReal x) : ℝ) = x :=
  rfl

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

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

Разделы

Аффилиация

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