nat_floor_real_sqrt_eq_nat_sqrt — Mathlib

English

For every a ∈ ℕ, ⌊√(a)⌋₊ = Nat.sqrt a.

Русский

Для любого a ∈ ℕ, ⌊√(a)⌋₊ = Nat.sqrt a.

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{N}, \\\\lfloor \\\\sqrt{(a \\\\in \\\\mathbb{R})} \\\\rfloor_{+} = \\\\operatorname{Nat}.sqrt a$$$

Lean4

/-- The natural floor of the real square root is the same as the natural square root. -/
@[simp]
theorem nat_floor_real_sqrt_eq_nat_sqrt {a : ℕ} : ⌊√(a : ℝ)⌋₊ = Nat.sqrt a :=
  by
  rw [Nat.floor_eq_iff (sqrt_nonneg a)]
  exact ⟨nat_sqrt_le_real_sqrt, real_sqrt_lt_nat_sqrt_succ⟩

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