algebraMap_eq_coe

Mathlib.Data.NNReal.Defs

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

English

The algebra map from ℝ≥0 to ℝ equals the standard coercion; i.e., algebraMap_{ℝ≥0→ℝ} = ↑.

Русский

Алгебраическое отображение из ℝ≥0 в ℝ равно обычному включению; algebraMap_{ℝ≥0→ℝ} = ↑.

LaTeX

$$$\text{algebraMap}_{\mathbb{R}_{\ge 0} \to \mathbb{R}} = \uparrow$$$

Lean4

@[simp, norm_cast]
theorem algebraMap_eq_coe : (algebraMap ℝ≥0 ℝ : ℝ≥0 → ℝ) = (↑) :=
  rfl

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

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

Разделы

Аффилиация

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