ratSqrt_nonneg

Mathlib.Data.Rat.NatSqrt.Defs

URI: https://scilib.ai/kg/mathlib#Nat.ratSqrt_nonneg

English

For any x and prec, ratSqrt(x, prec) is nonnegative: 0 ≤ ratSqrt(x, prec).

Русский

Для любых x и prec верно, что 0 ≤ ratSqrt(x, prec).

LaTeX

$$$ 0 \le \operatorname{ratSqrt}(x, \operatorname{prec}) $$$

Lean4

theorem ratSqrt_nonneg (x prec : ℕ) : 0 ≤ ratSqrt x prec :=
  by
  unfold ratSqrt
  positivity

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru