English
Let x,y ∈ ℝ with x ≥ 0 and y ≥ 0. Then x ≤ √y iff x^2 ≤ y.
Русский
Пусть x,y ∈ ℝ и x ≥ 0, y ≥ 0. Тогда x ≤ √y эквивалентно x^2 ≤ y.
LaTeX
$$$x \ge 0,\ y \ge 0 \Rightarrow (x \le \sqrt{y} \iff x^2 \le y)$$$
Lean4
/-- Note: if you want to conclude `x ≤ √y`, then use `Real.le_sqrt_of_sq_le`.
If you have `x > 0`, consider using `Real.le_sqrt'` -/
theorem le_sqrt (hx : 0 ≤ x) (hy : 0 ≤ y) : x ≤ √y ↔ x ^ 2 ≤ y :=
le_iff_le_iff_lt_iff_lt.2 <| sqrt_lt hy hx