sqrtTwoAddSeries_succ — Mathlib

English

For all x ∈ ℝ and n ∈ ℕ, sqrtTwoAddSeries x (n+1) = sqrtTwoAddSeries(√(2+x)) n.

Русский

Для всех x ∈ ℝ и n ∈ ℕ выполняется sqrtTwoAddSeries x (n+1) = sqrtTwoAddSeries(√(2+x)) n.

LaTeX

$$$\\sqrtTwoAddSeries x (n+1) = \\sqrtTwoAddSeries(\\sqrt{2+x}) \\ n$$$

Lean4

theorem sqrtTwoAddSeries_succ (x : ℝ) : ∀ n : ℕ, sqrtTwoAddSeries x (n + 1) = sqrtTwoAddSeries (√(2 + x)) n
  | 0 => rfl
  | n + 1 => by rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]

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