strictAntiOn_Ici_of_lt_pred — Mathlib

English

If ψ(m) < ψ(pred m) for all m > n, then ψ is strictly anti-monotone on Ici n.

Русский

Если ψ(m) > ψ(pred m) для m > n, то ψ строго анти монотонна на Ici n.

LaTeX

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

Lean4

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

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