sqrtTwoAddSeries_lt_two — Mathlib

English

For all n ∈ ℕ, sqrtTwoAddSeries 0 n < 2.

Русский

Для всех n ∈ ℕ: sqrtTwoAddSeries 0 n < 2.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\ sqrtTwoAddSeries(0, n) < 2$$$

Lean4

theorem sqrtTwoAddSeries_lt_two : ∀ n : ℕ, sqrtTwoAddSeries 0 n < 2
  | 0 => by simp
  | n + 1 => by
    refine lt_of_lt_of_le ?_ (sqrt_sq zero_lt_two.le).le
    rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']
    · refine (sqrtTwoAddSeries_lt_two n).trans_le ?_
      norm_num
    · exact add_nonneg zero_le_two (sqrtTwoAddSeries_zero_nonneg n)

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