exists_mem_Icc_isFixedPt — Mathlib

English

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

Русский

Если f непрерывна на Icc(a,b), то существует c ∈ Icc(a,b) такое что f(c) = c.

LaTeX

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

Lean4

/-- If `f : α → α` is continuous on `[a, b]`, `a ≤ b`, `a ≤ f a`, and `f b ≤ b`,
then `f` has a fixed point on `[a, b]`.

In particular, if `[a, b]` is forward-invariant under `f`,
then `f` has a fixed point on `[a, b]`, see `exists_mem_Icc_isFixedPt_of_mapsTo`. -/
theorem exists_mem_Icc_isFixedPt {a b : α} {f : α → α} (hf : ContinuousOn f (Icc a b)) (hle : a ≤ b) (ha : a ≤ f a)
    (hb : f b ≤ b) : ∃ c ∈ Icc a b, IsFixedPt f c :=
  isPreconnected_Icc.intermediate_value₂ (right_mem_Icc.2 hle) (left_mem_Icc.2 hle) hf continuousOn_id hb ha

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