antitone_iff_succ_le — Mathlib

English

A function on Fin(n+1) is antitone iff f(i+1) ≤ f(i) for all i.

Русский

Функция на Fin(n+1) антонна тогда и только тогда, когда f(i.succ) ≤ f(i.castSucc) для всех i.

LaTeX

$$$\mathrm{Antitone}(f) \iff ∀ i : \mathrm{Fin}\ n, f(i.succ) \le f(i.castSucc)$$$

Lean4

/-- A function `f` on `Fin (n + 1)` is antitone if and only if `f (i + 1) ≤ f i` for all `i`. -/
theorem antitone_iff_succ_le : Antitone f ↔ ∀ i : Fin n, f i.succ ≤ f (castSucc i) :=
  antitone_iff_forall_lt.trans <| liftFun_iff_succ (· ≥ ·)

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