nat_sqrt_le_real_sqrt — Mathlib

English

For all a ∈ ℕ, ↑Nat.sqrt(a) ≤ √(a:ℝ).

Русский

Для любого a ∈ ℕ, ↑Nat.sqrt(a) ≤ √(a:ℝ).

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{N}, \\\\uparrow(\\\\sqrt{a}) \\\\le \\\\sqrt{(a \\\\in \\\\mathbb{R})}$$$

Lean4

/-- The natural square root is at most the real square root -/
theorem nat_sqrt_le_real_sqrt {a : ℕ} : ↑(Nat.sqrt a) ≤ √(a : ℝ) :=
  by
  rw [Real.le_sqrt (Nat.cast_nonneg _) (Nat.cast_nonneg _)]
  norm_cast
  exact Nat.sqrt_le' a

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