coe_sqrt

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#Real.coe_sqrt

English

The real-valued square root commutes with the natural-coercion from NNReal: (√x as a real) equals √(x as real).

Русский

Корень в ℝ композиционен с отображением из ℝ≥0: (√x) в ℝ равен √(x в ℝ).

LaTeX

$$$ (\\sqrt{x} : \\mathbb{R}) = \\sqrt{(x : \\mathbb{R})}$$$

Lean4

@[simp, norm_cast]
theorem coe_sqrt {x : ℝ≥0} : (NNReal.sqrt x : ℝ) = √(x : ℝ) := by rw [Real.sqrt, Real.toNNReal_coe]

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

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

Разделы

Аффилиация

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