neg_sqrt_le_of_sq_le

Mathlib.Data.Real.Sqrt

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

English

If x^2 ≤ y then -√y ≤ x.

Русский

Если x^2 ≤ y, то -√y ≤ x.

LaTeX

$$$x^2 \le y \Rightarrow -\sqrt{y} \le x$$$

Lean4

theorem neg_sqrt_le_of_sq_le (h : x ^ 2 ≤ y) : -√y ≤ x :=
  ((sq_le ((sq_nonneg x).trans h)).mp h).1

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

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

Разделы

Аффилиация

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