succAbove_lt_iff_succ_le — Mathlib

English

For p ∈ Fin(n+1) and i ∈ Fin(n), p.succAbove i < p iff succ i ≤ p.

Русский

Для p ∈ Fin(n+1) и i ∈ Fin(n) выполняется p.succAbove i < p эквивалентно succ i ≤ p.

LaTeX

$$$\forall n \in \mathbb{N}\, \forall p \in \mathrm{Fin}(n+1)\, \forall i \in \mathrm{Fin}(n),\ p.succAbove(i) < p \Leftrightarrow \mathrm{succ}(i) \le p.$$$

Lean4

theorem succAbove_lt_iff_succ_le (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ succ i ≤ p := by
  rw [succAbove_lt_iff_castSucc_lt, castSucc_lt_iff_succ_le]

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