succAbove_of_castSucc_lt — Mathlib

English

Let n be a natural number, p ∈ Fin(n+1), and i ∈ Fin(n). If castSucc(i) < p, then p.succAbove(i) = castSucc(i).

Русский

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

LaTeX

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

Lean4

/-- Embedding `i : Fin n` into `Fin (n + 1)` with a hole around `p : Fin (n + 1)`
embeds `i` by `castSucc` when the resulting `i.castSucc < p`. -/
theorem succAbove_of_castSucc_lt (p : Fin (n + 1)) (i : Fin n) (h : castSucc i < p) : p.succAbove i = castSucc i :=
  if_pos h

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