sqrt_le_add

Mathlib.Data.Nat.Sqrt

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

English

For all n ∈ ℕ, n ≤ sqrt(n)^2 + 2 sqrt(n).

Русский

Для всех n ∈ ℕ верно n ≤ sqrt(n)^2 + 2 sqrt(n).

LaTeX

$$$n \le \sqrt{n}^2 + 2 \sqrt{n}$$$

Lean4

theorem sqrt_le_add (n : ℕ) : n ≤ sqrt n * sqrt n + sqrt n + sqrt n := by rw [← succ_mul];
  exact le_of_lt_succ (lt_succ_sqrt n)

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

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

Разделы

Аффилиация

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