predAbove_le_predAbove — Mathlib

English

If p ≤ q in Fin n and i ≤ j in Fin (n+1), then p.predAbove i ≤ q.predAbove j.

Русский

Если p ≤ q в Fin(n) и i ≤ j в Fin(n+1), то p.predAbove i ≤ q.predAbove j.

LaTeX

$$$\forall {n : \mathbb{N}} {p q : \mathrm{Fin}(n)}, hpq : p \le q \to \forall {i j : \mathrm{Fin}(n+1)}, hij : i \le j \to p.predAbove i \le q.predAbove j$$$

Lean4

@[gcongr]
theorem predAbove_le_predAbove {p q : Fin n} (hpq : p ≤ q) {i j : Fin (n + 1)} (hij : i ≤ j) :
    p.predAbove i ≤ q.predAbove j :=
  (predAbove_right_monotone p hij).trans (predAbove_left_monotone j hpq)

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