eq_sqrt'

Mathlib.Data.Nat.Sqrt

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

English

Let a, n be natural numbers. Then a = sqrt n iff a^2 ≤ n and n < (a+1)^2.

Русский

Пусть a, n ∈ ℕ. Тогда a = sqrt n тогда и только тогда, когда a^2 ≤ n и n < (a+1)^2.

LaTeX

$$$ a = \\sqrt{n} \\iff a^2 \\le n \\\\land n < (a+1)^2 $$$

Lean4

theorem eq_sqrt' : a = sqrt n ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2 := by simpa only [Nat.pow_two] using eq_sqrt

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

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

Разделы

Аффилиация

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