lt_succAbove_iff_lt_castSucc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lt_succAbove_iff_lt_castSucc (p : Fin (n + 1)) (i : Fin n) : p < p.succAbove i ↔ p < succ i := by
  rw [lt_succAbove_iff_le_castSucc, le_castSucc_iff]

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