exists_mem_uIcc_isFixedPt — Mathlib

English

If f on [a,b] is continuous, then there exists c ∈ [a,b] with f(c) = c.

Русский

Пусть f на [a,b] непрерывна. Тогда существует c ∈ [a,b], такое что f(c) = c.

LaTeX

$$∃ c ∈ Icc(a,b), f(c) = c$$

Lean4

/-- If `f : α → α` is continuous on `[[a, b]]`, `a ≤ f a`, and `f b ≤ b`,
then `f` has a fixed point on `[[a, b]]`. -/
theorem exists_mem_uIcc_isFixedPt {a b : α} {f : α → α} (hf : ContinuousOn f (uIcc a b)) (ha : a ≤ f a) (hb : f b ≤ b) :
    ∃ c ∈ [[a, b]], IsFixedPt f c :=
  isPreconnected_uIcc.intermediate_value₂ right_mem_uIcc left_mem_uIcc hf continuousOn_id hb ha

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