eq_sqrt — Mathlib

English

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

Русский

Пусть n, a ∈ ℕ. Тогда 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 * a ≤ n ∧ n < (a + 1) * (a + 1) :=
  ⟨fun e ↦ e.symm ▸ sqrt_isSqrt n, fun ⟨h₁, h₂⟩ ↦ le_antisymm (le_sqrt.2 h₁) (le_of_lt_succ <| sqrt_lt.2 h₂)⟩

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