mem_range_of_exists_le_of_exists_ge

English

Same as above: if there exist a,b with f(a) ≤ c ≤ f(b) and f is continuous, then c is in the range of f.

Русский

Аналогично; если существуют точки a,b такие, что f(a) ≤ c ≤ f(b) и f непрерывна, то c принадлежит образу f.

LaTeX

$$$\text{Continuous}(f) \land (\exists a\, f(a) \le c) \land (\exists b\, c \le f(b)) \Rightarrow c \in \mathrm{range}(f)$$$

Lean4

/-- **Intermediate Value Theorem** for continuous functions on connected spaces. -/
theorem mem_range_of_exists_le_of_exists_ge [PreconnectedSpace X] {c : α} {f : X → α} (hf : Continuous f)
    (h₁ : ∃ a, f a ≤ c) (h₂ : ∃ b, c ≤ f b) : c ∈ range f :=
  let ⟨a, ha⟩ := h₁;
  let ⟨b, hb⟩ := h₂;
  intermediate_value_univ a b hf ⟨ha, hb⟩

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