sqrt_eq_zero

Mathlib.Data.Real.Sqrt

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

English

For NNReal x, sqrt x = 0 iff x = 0.

Русский

Для NNReal x, sqrt x = 0 тогда и только тогда, когда x = 0.

LaTeX

$$$\forall x \in \mathbb{R}_{\ge 0},\ \sqrt{x} = 0 \iff x = 0$$$

Lean4

@[simp]
theorem sqrt_eq_zero : sqrt x = 0 ↔ x = 0 := by simp [sqrt_eq_iff_eq_sq]

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

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

Разделы

Аффилиация

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