sq_sqrt

Mathlib.Data.Real.Sqrt

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

English

For any NNReal x, (sqrt x)^2 = x.

Русский

Для любого x ∈ NNReal выполняется (sqrt x)^2 = x.

LaTeX

$$$\forall x \in \mathbb{R}_{\ge 0}, (\sqrt x)^2 = x$$$

Lean4

@[simp]
theorem sq_sqrt (x : ℝ≥0) : sqrt x ^ 2 = x :=
  sqrt.symm_apply_apply _

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

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

Разделы

Аффилиация

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