sqrt_eq_zero'

Mathlib.Data.Real.Sqrt

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

English

√x = 0 iff x ≤ 0.

Русский

√x = 0 эквивалентно x ≤ 0.

LaTeX

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

Lean4

theorem sqrt_eq_zero' : √x = 0 ↔ x ≤ 0 := by rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]

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

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

Разделы

Аффилиация

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