ratSqrt_le_realSqrt — Mathlib

English

For x ∈ ℕ and prec > 0, ratSqrt(x, prec) ≤ √x when viewed in ℝ.

Русский

Для x ∈ ℕ и prec > 0,RatSqrt(x, prec) ≤ √x при отображении в ℝ.

LaTeX

$$$ \operatorname{ratSqrt}(x, \operatorname{prec}) \le \sqrt{x} \quad (x \in \mathbb{N}, \operatorname{prec} > 0) $$$

Lean4

theorem ratSqrt_le_realSqrt (x : ℕ) {prec : ℕ} (h : 0 < prec) : ratSqrt x prec ≤ √x :=
  by
  have := ratSqrt_sq_le (x := x) h
  have : (x.ratSqrt prec ^ 2 : ℝ) ≤ ↑x := by norm_cast
  have := Real.sqrt_monotone this
  rwa [Real.sqrt_sq] at this
  simpa only [Rat.cast_nonneg] using ratSqrt_nonneg _ _

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