le_sqrt — Mathlib

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

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