ωSup_iterate_le_prefixedPoint — Mathlib

English

If f is left order continuous and s has a greatest element x, then f''s has greatest element f x.

Русский

Если f слева непрерывна и множество s имеет наибольший элемент x, то образ f''s имеет наибольший элемент f x.

LaTeX

$$$\text{IsGreatest}(s,x)\Rightarrow \text{IsGreatest}(f''s,f x)$$$

Lean4

/-- The supremum of iterating a function on x arbitrary often is smaller than any prefixed point.

A prefixed point is a value `a` with `f a ≤ a`. -/
theorem ωSup_iterate_le_prefixedPoint (h : x ≤ f x) {a : α} (h_a : f a ≤ a) (h_x_le_a : x ≤ a) :
    ωSup (iterateChain f x h) ≤ a := by
  apply ωSup_le
  intro n
  induction n with
  | zero => exact h_x_le_a
  | succ n
    h_ind =>
    have : iterateChain f x h (n.succ) = f (iterateChain f x h n) := Function.iterate_succ_apply' ..
    rw [this]
    exact le_trans (f.monotone h_ind) h_a

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