sqrt_one_add_le — Mathlib

English

If h ≥ 0, then √(1+h) ≤ 1 + h/2.

Русский

Если h ≥ 0, то √(1+h) ≤ 1 + h/2.

LaTeX

$$$\\\\forall h \\\\in \\\\mathbb{R}, -1 \\\\le h \\\\Rightarrow \\\\sqrt{1+h} \\\\le 1 + h/2$$$

Lean4

/-- Bernoulli's inequality for exponent `1 / 2`, stated using `sqrt`. -/
theorem sqrt_one_add_le (h : -1 ≤ x) : √(1 + x) ≤ 1 + x / 2 :=
  by
  refine sqrt_le_iff.mpr ⟨by linarith, ?_⟩
  calc
    1 + x
    _ ≤ 1 + x + (x / 2) ^ 2 := (le_add_of_nonneg_right <| sq_nonneg _)
    _ = _ := by ring

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