sq_sqrt'

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#Real.sq_sqrt'

← MathLib Explorer

English

For all x, (√x)^2 = max{x,0}.

Русский

Для любого x выполняется (√x)^2 = max{x,0}.

LaTeX

$$$(\sqrt{x})^2 = \max\{x,0\}$$$

Lean4

/-- Variant of `sq_sqrt` without a non-negativity assumption on `x`. -/
theorem sq_sqrt' : √x ^ 2 = max x 0 := by
  rcases lt_trichotomy x 0 with _ | _ | _ <;>
    grind [sqrt_eq_zero', sq_sqrt]
      -- Add the rule for `√x ^ 2` to the grind whiteboard whenever we see a real square root.

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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