succAboveCases — Mathlib

English

There is a canonical equivalence between a tailed n+1-tuple and a head element together with an n-tuple obtained by casting.

Русский

Существует каноническая эквивалентность между кортежем длины n+1 и парой: последняя часть и n-часть с cast.

LaTeX

$$$\\\\text{snocEquiv} : (\\\\alpha(\\\\mathrm{last} n) \\times (\\\\forall i, \\\\alpha(\\\\castSucc i))) \\\\simeq \\\\forall i, \\\\alpha i$$$

Lean4

/-- Define a function on `Fin (n + 1)` from a value on `i : Fin (n + 1)` and values on each
`Fin.succAbove i j`, `j : Fin n`. This version is elaborated as eliminator and works for
propositions, see also `Fin.insertNth` for a version without an `@[elab_as_elim]`
attribute. -/
@[elab_as_elim]
def succAboveCases {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : ∀ j : Fin n, α (i.succAbove j))
    (j : Fin (n + 1)) : α j :=
  if hj : j = i then Eq.rec x hj.symm
  else
    if hlt : j < i then (succAbove_castPred_of_lt _ _ hlt) ▸ (p _)
    else
      (succAbove_pred_of_lt _ _ <| (Fin.lt_or_lt_of_ne hj).resolve_left hlt) ▸
        (p _)
          -- This is a duplicate of `Fin.exists_fin_succ` in Core. We should upstream the name change.

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