English
If f is left order continuous, then each finite iterate f^[n] is left order continuous.
Русский
Если f слева непрерывна по порядку, то каждый конечный итерат f^[n] тоже слева непрерывный по порядку.
LaTeX
$$$\text{LeftOrdContinuous}(f) \Rightarrow \forall n:\mathbb{N},\ \text{LeftOrdContinuous}(f^{[n]})$$$
Lean4
/-- The supremum of iterating a function on x arbitrary often is a fixed point -/
theorem ωSup_iterate_mem_fixedPoint (h : x ≤ f x) : ωSup (iterateChain f x h) ∈ fixedPoints f :=
by
rw [mem_fixedPoints, IsFixedPt, f.continuous]
apply le_antisymm
· apply ωSup_le
intro n
simp only [Chain.map_coe, OrderHomClass.coe_coe, comp_apply]
have : iterateChain f x h (n.succ) = f (iterateChain f x h n) := Function.iterate_succ_apply' ..
rw [← this]
apply le_ωSup
· apply ωSup_le
rintro (_ | n)
· apply le_trans h
change ((iterateChain f x h).map f) 0 ≤ ωSup ((iterateChain f x h).map (f : α →o α))
apply le_ωSup
· have : iterateChain f x h (n.succ) = (iterateChain f x h).map f n := Function.iterate_succ_apply' ..
rw [this]
apply le_ωSup
