ratSqrt_mem_Ioc — Mathlib

English

For x ∈ ℕ and prec > 0, the real value of ratSqrt(x, prec) lies in the half-open interval (√x − 1/prec, √x].

Русский

Для x ∈ ℕ и prec > 0 вещественное значение ratSqrt(x, prec) лежит в интервале (√x − 1/prec, √x].

LaTeX

$$$ (\operatorname{ratSqrt}(x, \operatorname{prec}) : \mathbb{R}) \in \left( \sqrt{x} - \frac{1}{\operatorname{prec}}, \sqrt{x} \right] $$$

Lean4

theorem ratSqrt_mem_Ioc (x : ℕ) {prec : ℕ} (h : 0 < prec) : (ratSqrt x prec : ℝ) ∈ Set.Ioc (√x - 1 / prec) √x := by
  grind [ratSqrt_le_realSqrt]

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