not_exists_sq'

Mathlib.Data.Nat.Sqrt

URI: https://scilib.ai/kg/mathlib#Nat.not_exists_sq'

English

m^2 < n and n < (m+1)^2 imply not exists t with t^2 = n.

Русский

Если m^2 < n и n < (m+1)^2, то не существует t, такого что t^2 = n.

LaTeX

$$$ m^2 < n \\Rightarrow n < (m+1)^2 \\Rightarrow \\neg ∃ t, t^2 = n $$$

Lean4

theorem not_exists_sq' : m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ t, t ^ 2 = n := by
  simpa only [Nat.pow_two] using not_exists_sq

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

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

Разделы

Аффилиация

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