English
If φ is pointwise monotone (i ≤ φ i for all i), then the map j ↦ transfiniteIterate φ j i₀ is monotone in j.
Русский
Если \u03c6 удовлетворяет условию i ≤ φ i для всех i, то отображение j ↦ transfiniteIterate φ j i₀ монотонно по j.
LaTeX
$$$\\forall i, i \\le φ(i) \\Rightarrow (j \\le k) \\Rightarrow transfiniteIterate φ j i_0 \\le transfiniteIterate φ k i_0$$$
Lean4
theorem monotone_transfiniteIterate (hφ : ∀ (i : I), i ≤ φ i) : Monotone (fun (j : J) ↦ transfiniteIterate φ j i₀) :=
by
intro k j hkj
induction j using SuccOrder.limitRecOn with
| isMin k hk =>
obtain rfl := hk.eq_bot
obtain rfl : k = ⊥ := by simpa using hkj
rfl
| succ k' hk' hkk' =>
obtain hkj | rfl := hkj.lt_or_eq
· refine (hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_
dsimp
rw [transfiniteIterate_succ _ _ _ hk']
apply hφ
· rfl
| isSuccLimit k' hk' _ =>
obtain hkj | rfl := hkj.lt_or_eq
· dsimp
rw [transfiniteIterate_limit _ _ _ hk']
exact le_iSup (fun (⟨l, hl⟩ : Set.Iio k') ↦ transfiniteIterate φ l i₀) ⟨k, hkj⟩
· rfl
