lean_workbook_plus_58814
ProvedGiven , ...... , , ...... are positive real numbers satisfying + < 2. Prove that there exist two positive integers k, m (k, m = 1, 2, ..., 7) such that | |+| |<1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58814 (a b : Fin 7 → ℝ) (ha : ∀ i, 0 < a i) (hb : ∀ i, 0 < b i) (hab : ∀ i, a i + b i < 2) : ∃ k m, |a k - a m| + |b k - b m| < 1 := by sorry
Source