le_sqrt_of_sq_le

Mathlib.Data.Real.Sqrt

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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