surjOn_uIcc — Mathlib

English

If s is order-connected and f is continuous on s, then f[s] contains the closed interval uIcc(f(a), f(b)).

Русский

Если s неразделимо по порядку и f непрерывна на s, тогда образ f[s] содержит замкнутый интервал uIcc(f(a), f(b)).

LaTeX

$$SurjOn f s (uIcc (f a) (f b))$$

Lean4

/-- **Intermediate value theorem**: if `f` is continuous on an order-connected set `s` and `a`,
`b` are two points of this set, then `f` sends `s` to a superset of `[f x, f y]`. -/
theorem surjOn_uIcc {s : Set α} [hs : OrdConnected s] {f : α → δ} (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) : SurjOn f s (uIcc (f a) (f b)) := by
  rcases le_total (f a) (f b) with hab | hab <;> simp [hf.surjOn_Icc, *]

Похожие утверждения