English
For x ∈ ℕ and prec > 0, the real number √x lies in the interval [ratSqrt(x, prec), ratSqrt(x, prec) + 1/prec) when both are viewed as real numbers.
Русский
Для x ∈ ℕ и prec > 0 число √x принадлежит промежутку [ratSqrt(x, prec), ratSqrt(x, prec) + 1/prec) при отображении в ℝ.
LaTeX
$$$ \sqrt{x} \in \left[ \operatorname{ratSqrt}(x, \operatorname{prec}), \operatorname{ratSqrt}(x, \operatorname{prec}) + \frac{1}{\operatorname{prec}} \right) \;\text{in } \mathbb{R} $$$
Lean4
theorem realSqrt_mem_Ico (x : ℕ) {prec : ℕ} (h : 0 < prec) :
√x ∈ Set.Ico (ratSqrt x prec : ℝ) (ratSqrt x prec + 1 / prec : ℝ) := by
grind [ratSqrt_le_realSqrt, realSqrt_lt_ratSqrt_add_inv_prec]
