minFac_lemma

Mathlib.Data.Nat.Prime.Defs

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

← MathLib Explorer

English

If n ≥ k^2, then sqrt(n) − k < sqrt(n) + 2 − k.

Русский

Если n ≥ k^2, тогда √n − k < √n + 2 − k.

LaTeX

$$$\\\\forall n,k \\\\in \\\\mathbb{N}, \\\\text{n} \\\\ge k^2 \\\\Rightarrow \\\\sqrt{n} - k < \\\\sqrt{n} + 2 - k.$$$

Lean4

theorem minFac_lemma (n k : ℕ) (h : ¬n < k * k) : sqrt n - k < sqrt n + 2 - k :=
  (Nat.sub_lt_sub_right <| le_sqrt.2 <| le_of_not_gt h) <| Nat.lt_add_of_pos_right (by decide)

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

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

Разделы

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

Аффилиация

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