ratSqrt_sq_le — Mathlib

English

For x ∈ ℕ and prec > 0, the square of ratSqrt(x, prec) does not exceed x: (ratSqrt(x, prec))^2 ≤ x.

Русский

Для натурального x и prec > 0 верно (ratSqrt(x, prec))^2 ≤ x.

LaTeX

$$$ (\operatorname{ratSqrt}(x, \operatorname{prec}))^2 \le x, \quad (0 < \operatorname{prec}) $$$

Lean4

theorem ratSqrt_sq_le (x : ℕ) {prec : ℕ} (h : 0 < prec) : (ratSqrt x prec) ^ 2 ≤ x :=
  by
  unfold ratSqrt
  rw [div_pow, div_le_iff₀ (by positivity)]
  norm_cast
  exact sqrt_le' (x * prec ^ 2)

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