abs_le_sqrt_iff_sq_le

Mathlib.Data.Int.Order.Lemmas

URI: https://scilib.ai/kg/mathlib#Int.abs_le_sqrt_iff_sq_le

English

For integers a,b with b ≥ 0, |a| ≤ sqrt(b) if and only if a^2 ≤ b.

Русский

Для целых a,b с b ≥ 0 выполняется: |a| ≤ sqrt(b) тогда и только тогда, когда a^2 ≤ b.

LaTeX

$$$\forall a,b \in \mathbb{Z}, b \ge 0 \Rightarrow |a| \le \sqrt{b} \iff a^2 \le b.$$$

Lean4

theorem abs_le_sqrt_iff_sq_le {a b : ℤ} (hn : 0 ≤ b) : |a| ≤ b.sqrt ↔ a ^ 2 ≤ b :=
  pow_two a ▸ abs_le_sqrt hn

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

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

Разделы

Аффилиация

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