lean_workbook_plus_20581
Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
f(0)=f(5)=−1⟹f(t)≤−1,∀t∈[0,5]⟹\n ⟹∣f(t)∣≥1,∀t∈[0,5] .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20581 (f : ℝ → ℝ)
(h₀ : f 0 = -1)
(h₁ : f (Real.sqrt 5) = -1)
(h₂ : ∀ t ∈ Set.Icc 0 (Real.sqrt 5), f t ≤ -1) :
∀ t ∈ Set.Icc 0 (Real.sqrt 5), 1 ≤ |f t| := by sorry
View graph