lean_workbook_plus_64280
ProvedProve that at least one among is less than given for positive real numbers and a positive integer .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64280 (n : ℕ) (a : Fin n → ℝ) (h : ∑ i, a i < n) : ∃ i, a i < 1 := by sorry
Source