Limit_of_Function_in_Interval
Provedanalysislimitsproofwikireal-analysis
If f maps (a,b) into [a,b] and f(x) -> l as x -> xi in (a,b), then a <= l <= b.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_of_Function_in_Interval (f : ℝ → ℝ) (a b ξ l : ℝ) (hab : a < b) (hξ : ξ ∈ Set.Ioo a b) (hf : ∀ x ∈ Set.Ioo a b, a ≤ f x ∧ f x ≤ b) (hlim : Filter.Tendsto f (nhdsWithin ξ (Set.Ioo a b)) (nhds l)) : a ≤ l ∧ l ≤ b := by sorry
Source