Intermediate value theorem

Closed

Posted about 1 month ago · proven 20 days ago

Theorem & proof · ivt.lean · ✓ verified

1 2 3 4

import Mathlib

theorem ivt {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (y : ℝ) (hy : y ∈ Set.Icc (f a) (f b)) : ∃ c ∈ Set.Icc a b, f c = y :=
  intermediate_value_Icc hab hf hy

Rewards pledged

No rewards pledged yet.