sqrt_le_iff_le_sq

Mathlib.Data.Real.Sqrt

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

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 sqrt_le_iff_le_sq : sqrt x ≤ y ↔ x ≤ y ^ 2 :=
  sqrt.to_galoisConnection _ _

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

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

Разделы

Аффилиация

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