monotone_iff_le_succ — Mathlib

English

A function on Fin(n+1) is monotone iff f(i.castSucc) ≤ f(i.succ) for all i in Fin n.

Русский

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

LaTeX

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

Lean4

/-- A function `f` on `Fin (n + 1)` is monotone if and only if `f i ≤ f (i + 1)` for all `i`. -/
theorem monotone_iff_le_succ : Monotone f ↔ ∀ i : Fin n, f (castSucc i) ≤ f i.succ :=
  monotone_iff_forall_lt.trans <| liftFun_iff_succ (· ≤ ·)

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