real_sqrt_le_nat_sqrt_succ

Mathlib.Data.Real.Sqrt

URI: https://scilib.ai/kg/mathlib#Real.real_sqrt_le_nat_sqrt_succ

← MathLib Explorer

English

For every natural a, √a ≤ Nat.sqrt a + 1.

Русский

Для каждого натурального a верно: √a ≤ Nat.sqrt a + 1.

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{N}, \\\\sqrt{a} \\\\le \\\\operatorname{Nat}.sqrt a + 1$$$

Lean4

/-- The real square root is at most the natural square root plus one -/
theorem real_sqrt_le_nat_sqrt_succ {a : ℕ} : √(a : ℝ) ≤ Nat.sqrt a + 1 :=
  real_sqrt_lt_nat_sqrt_succ.le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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