English
If α is a SuccOrder and IsSuccArchimedean, then for any n, a condition that ψ(m) < ψ(succ m) for all m < n implies ψ is strictly monotone on Iic n.
Русский
Пусть α — бинарный порядок с переходом к следующему; если для всех m < n выполняется ψ(m) < ψ(succ(m)), то ψ строго монотонна на промежутке Iic(n).
LaTeX
$$$\forall x,y ∈ \mathrm{Iic}(n), x < y \Rightarrow ψ(x) < ψ(y).$$$
Lean4
/-- A function `ψ` on a `SuccOrder` is strictly monotone before some `n` if for all `m` such that
`m < n`, we have `ψ m < ψ (succ m)`. -/
theorem strictMonoOn_Iic_of_lt_succ [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : ∀ m, m < n → ψ m < ψ (succ m)) :
StrictMonoOn ψ (Set.Iic n) :=
strictMonoOn_of_lt_succ ordConnected_Iic fun _a ha' _ ha ↦ hψ _ <| (succ_le_iff_of_not_isMax ha').1 ha
