intermediate_value — Mathlib

English

For continuous f on a preconnected X, if f a ≤ g a and g b ≤ f b for endpoints a,b, then there is x with f(x) = g(x).

Русский

Для непрерывных f,g на предсоединенном X: если f(a) ≤ g(a) и g(b) ≤ f(b) на концах, тогда существует x с f(x) = g(x).

LaTeX

$$$\\exists x: X, f(x) = g(x).$$$

Lean4

/-- **Intermediate Value Theorem** for continuous functions on connected sets. -/
theorem intermediate_value {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f : X → α}
    (hf : ContinuousOn f s) : Icc (f a) (f b) ⊆ f '' s := fun _x hx =>
  hs.intermediate_value₂ ha hb hf continuousOn_const hx.1 hx.2

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