strictMonoOn_Ici_of_pred_lt — Mathlib

English

If ψ(m-1) < ψ(m) whenever m > n (PredOrder setting), then ψ is strictly monotone on Ici n.

Русский

Пусть для m > n выполняется ψ(pred m) < ψ(m); тогда ψ строго возрастает на Ici n.

LaTeX

$$$\forall x,y \in \mathrm{Ici}(n), x < y \Rightarrow ψ(x) < ψ(y).$$$

Lean4

theorem strictMonoOn_Ici_of_pred_lt [PredOrder α] [IsPredArchimedean α] {n : α} (hψ : ∀ m, n < m → ψ (pred m) < ψ m) :
    StrictMonoOn ψ (Set.Ici n) := fun i hi j hj hij => @strictMonoOn_Iic_of_lt_succ αᵒᵈ βᵒᵈ _ _ ψ _ _ n hψ j hj i hi hij

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