lean_workbook_plus_81405

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Since $x_n^2$ is the highest square, all other $x_i^2$ are in $[-x_n^2, x_n^2]$ , so each $x_i$ is in $[-|x_n|, |x_n|]$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81405  (x : ℕ → ℝ)
  (n : ℕ)
  (h₀ : 0 < n)
  (h₁ : ∀ i, 0 ≤ x i)
  (h₂ : ∀ i, x i^2 ≤ x n^2) :
  ∀ i, -|x n| ≤ x i ∧ x i ≤ |x n|   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph