coe_two

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.coe_two

English

Coercion of two: ((2 : NNReal) : ℝ) = 2.

Русский

Коэрцирование двойки: ((2 : NNReal) : ℝ) = 2.

LaTeX

$$$ ((2 : \mathbb{R}_{\ge 0}) : \mathbb{R}) = 2 $$$

Lean4

protected theorem coe_two : ((2 : ℝ≥0) : ℝ) = 2 :=
  rfl

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

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

Разделы

Аффилиация

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