le_sqrt_iff_sq_le

Mathlib.Data.Real.Sqrt

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

English

For NNReal x,y, sqrt x ≤ y iff x ≤ y^2.

Русский

Для NNReal x,y верно: sqrt x ≤ y ⇔ x ≤ y^2.

LaTeX

$$$\forall x,y \in \mathbb{R}_{\ge 0},\ \sqrt{x} \le y \iff x \le y^{2}$$$

Lean4

theorem le_sqrt_iff_sq_le : x ≤ sqrt y ↔ x ^ 2 ≤ y :=
  (sqrt.symm.to_galoisConnection _ _).symm

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

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

Разделы

Аффилиация

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