strictMono_succAbove — Mathlib

English

For any p in Fin(n+1), the map i ↦ succAbove p i is strictly increasing.

Русский

Для любого p ∈ Fin(n+1) отображение i ↦ succAbove p i строго возрастает.

LaTeX

$$$\forall p:\mathrm{Fin}(n+1), \mathrm{StrictMono}(\mathrm{succAbove}(p))$$$

Lean4

theorem strictMono_succAbove (p : Fin (n + 1)) : StrictMono (succAbove p) :=
  strictMono_castSucc.ite strictMono_succ (fun _ _ hij hj => (castSucc_lt_castSucc_iff.mpr hij).trans hj) fun i =>
    (castSucc_lt_succ i).le

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