strictAntiOn_Iic_of_succ_lt — Mathlib

English

If ψ(m+1) < ψ(m) for all m < n, then ψ is strictly anti-monotone on Iic n.

Русский

Если для всех m < n имеет место ψ(succ m) < ψ(m), то ψ антимонотонна на Iic(n).

LaTeX

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

Lean4

theorem strictAntiOn_Iic_of_succ_lt [SuccOrder α] [IsSuccArchimedean α] {n : α} (hψ : ∀ m, m < n → ψ (succ m) < ψ m) :
    StrictAntiOn ψ (Set.Iic n) := fun i hi j hj hij => @strictMonoOn_Iic_of_lt_succ α βᵒᵈ _ _ ψ _ _ n hψ i hi j hj hij

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