sqrtTwoAddSeries_monotone_left — Mathlib

English

If x ≤ y, then for all n ∈ ℕ, sqrtTwoAddSeries x n ≤ sqrtTwoAddSeries y n.

Русский

Если x ≤ y, то для каждого n ∈ ℕ верно: sqrtTwoAddSeries x n ≤ sqrtTwoAddSeries y n.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\ sqrtTwoAddSeries(x,n) \\le \\ sqrtTwoAddSeries(y,n) \\Rightarrow \\ x \\le \\ y$$$

Lean4

theorem sqrtTwoAddSeries_monotone_left {x y : ℝ} (h : x ≤ y) : ∀ n : ℕ, sqrtTwoAddSeries x n ≤ sqrtTwoAddSeries y n
  | 0 => h
  | n + 1 => by
    rw [sqrtTwoAddSeries, sqrtTwoAddSeries]
    exact sqrt_le_sqrt (add_le_add_left (sqrtTwoAddSeries_monotone_left h _) _)

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