sqrt_nonneg

Mathlib.Data.Real.Sqrt

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

English

For every real x, the square root is nonnegative: 0 ≤ √x.

Русский

Для любого x ∈ ℝ корень неотрицателен: 0 ≤ √x.

LaTeX

$$$0 \le \sqrt{x}$$$

Lean4

@[simp]
theorem sqrt_nonneg (x : ℝ) : 0 ≤ √x :=
  NNReal.coe_nonneg _

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

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

Разделы

Аффилиация

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