sqrt_lt_self

Mathlib.Data.Nat.Sqrt

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

English

If 1 < n, then sqrt n < n.

Русский

Если 1 < n, то sqrt n < n.

LaTeX

$$$1 < n \\Rightarrow \\sqrt{n} < n$$$

Lean4

theorem sqrt_lt_self (h : 1 < n) : sqrt n < n :=
  sqrt_lt.2 <| by have := Nat.mul_lt_mul_of_pos_left h (lt_of_succ_lt h); grind

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

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

Разделы

Аффилиация

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