surjOn_Icc — Mathlib

English

If s is order-connected and f is continuous on s, then the image f[s] contains the closed interval Icc(f(a), f(b)) for any a, b ∈ s.

Русский

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

LaTeX

$$SurjOn f s (Icc (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 `Icc (f x) (f y)`. -/
theorem surjOn_Icc {s : Set α} [hs : OrdConnected s] {f : α → δ} (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) : SurjOn f s (Icc (f a) (f b)) :=
  hs.isPreconnected.intermediate_value ha hb hf

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