exists_mem_Icc_isFixedPt_of_mapsTo

English

If a closed interval [a,b] is forward-invariant under a continuous map f, there exists a fixed point c ∈ [a,b].

Русский

Если [a,b] отображается в себя непрерывной картой f, существует фиксированная точка c ∈ [a,b].

LaTeX

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

Lean4

/-- If a closed interval is forward-invariant under a continuous map `f : α → α`,
then this map has a fixed point on this interval. -/
theorem exists_mem_Icc_isFixedPt_of_mapsTo {a b : α} {f : α → α} (hf : ContinuousOn f (Icc a b)) (hle : a ≤ b)
    (hmaps : MapsTo f (Icc a b) (Icc a b)) : ∃ c ∈ Icc a b, IsFixedPt f c :=
  exists_mem_Icc_isFixedPt hf hle (hmaps <| left_mem_Icc.2 hle).1 (hmaps <| right_mem_Icc.2 hle).2

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