English
If φ is strictly monotone on Iic n in a suitable ordered setting, then for all m ≤ n, m ≤ φ(m).
Русский
Если φ строго монотонна на Iic n в подходящей структуре порядка, то для всех m ≤ n выполняется m ≤ φ(m).
LaTeX
$$$\forall m \le n,\ m \le φ(m).$$$
Lean4
theorem Iic_id_le [SuccOrder α] [IsSuccArchimedean α] [OrderBot α] {n : α} {φ : α → α}
(hφ : StrictMonoOn φ (Set.Iic n)) : ∀ m ≤ n, m ≤ φ m :=
by
revert hφ
refine Succ.rec_bot (fun n => StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m) (fun _ _ hm => hm.trans bot_le) ?_ _
rintro k ih hφ m hm
by_cases hk : IsMax k
· rw [succ_eq_iff_isMax.2 hk] at hm
exact ih (hφ.mono <| Iic_subset_Iic.2 (le_succ _)) _ hm
obtain rfl | h := le_succ_iff_eq_or_le.1 hm
· specialize ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) k le_rfl
nth_grw 1 [ih]
refine succ_le_of_lt (hφ (le_succ _) le_rfl ?_)
exact lt_succ_of_not_isMax hk
· exact ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) _ h
