snoc_castSucc — Mathlib

English

The snoc construction commutes with the castSucc operation on indices: the image under the embedding is preserved when shifting index by one.

Русский

Конструкция snoc сохраняет индексы при переходе через castSucc: отображение сохраняется при сдвиге индекса на единицу.

LaTeX

$$$\text{snoc}_{ n} (x)^{castSucc} = x$$$

Lean4

theorem snoc_castSucc {n : ℕ} {x : Fin n ↪ α} {a : α} {ha : a ∉ range x} {i : Fin n} : snoc x ha i.castSucc = x i := by
  rw [coe_snoc, Fin.snoc_castSucc]

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