ωSup_iterate_le_fixedPoint — Mathlib

English

If h: x ≤ f x and a is a prefixed point (f a ≤ a) with x ≤ a, then ωSup (iterateChain f x h) ≤ a.

Русский

Если h: x ≤ f x и a — префиксная точка (f a ≤ a) с x ≤ a, то ωSup (iterateChain f x h) ≤ a.

LaTeX

$$$ h: x\le f x \Rightarrow (f a \le a) \Rightarrow (x\le a) \Rightarrow ωSup (iterateChain\ f\ x\ h) \le a$$$

Lean4

/-- The supremum of iterating a function on x arbitrary often is smaller than any fixed point. -/
theorem ωSup_iterate_le_fixedPoint (h : x ≤ f x) {a : α} (h_a : a ∈ fixedPoints f) (h_x_le_a : x ≤ a) :
    ωSup (iterateChain f x h) ≤ a := by
  rw [mem_fixedPoints] at h_a
  obtain h_a := Eq.le h_a
  exact ωSup_iterate_le_prefixedPoint f x h h_a h_x_le_a

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