sqrt_eq_zero_of_nonpos

Mathlib.Data.Real.Sqrt

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

English

If x ≤ 0, then √x = 0.

Русский

Пусть x ≤ 0. Тогда √x = 0.

LaTeX

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

Lean4

theorem sqrt_eq_zero_of_nonpos (h : x ≤ 0) : sqrt x = 0 := by simp [sqrt, Real.toNNReal_eq_zero.2 h]

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

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

Разделы

Аффилиация

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