Prove2Me

lean_workbook_plus_69508

Proved

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

For k∈{1,2,...,n}k \in \{1,2,...,n\} we have (xk−x1)≥0(x_{k}-x_{1})\ge 0 and (xk−xn)≤0(x_{k}-x_{n})\le 0 .Therefore (∗)      (xk−x1)(xk−xn)≤0    ,  ∀k∈{1,2,...,n}.(*)\; \; \; (x_{k}-x_{1})(x_{k}-x_{n})\le 0 \; \; ,\; \forall k \in \{1,2,...,n\}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69508  (n : ℕ)
  (x : ℕ → ℝ)
  (h₀ : 0 < n)
  (h₁ : ∀ k, 1 ≤ k ∧ k ≤ n → (x k - x 1) ≥ 0)
  (h₂ : ∀ k, 1 ≤ k ∧ k ≤ n → (x k - x n) ≤ 0) :
  ∀ k, 1 ≤ k ∧ k ≤ n → (x k - x 1) * (x k - x n) ≤ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph