strictMono_iff_lt_succ — Mathlib

English

A function on Fin(n+1) is strictly monotone iff f(i) < f(i+1) for all i in Fin n.

Русский

Функция на Fin(n+1) строго возрастает тогда и только тогда, когда для всех i в Fin n выполняется f(i) < f(i+1).

LaTeX

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

Lean4

/-- A function `f` on `Fin (n + 1)` is strictly monotone if and only if `f i < f (i + 1)`
for all `i`. -/
theorem strictMono_iff_lt_succ : StrictMono f ↔ ∀ i : Fin n, f (castSucc i) < f i.succ :=
  liftFun_iff_succ (· < ·)

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