succAbove_of_le_castSucc — Mathlib

English

Let p ∈ Fin(n+1) and i ∈ Fin(n). If p ≤ castSucc(i), then p.succAbove(i) = i.succ.

Русский

Пусть p ∈ Fin(n+1) и i ∈ Fin(n). Если p ≤ castSucc(i), тогда p.succAbove(i) = i.succ.

LaTeX

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

Lean4

/-- Embedding `i : Fin n` into `Fin (n + 1)` with a hole around `p : Fin (n + 1)`
embeds `i` by `succ` when the resulting `p < i.succ`. -/
theorem succAbove_of_le_castSucc (p : Fin (n + 1)) (i : Fin n) (h : p ≤ castSucc i) : p.succAbove i = i.succ :=
  if_neg (Fin.not_lt.2 h)

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