strictAnti_iff_succ_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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