cons_self_tail — Mathlib

English

There is a canonical equivalence between α0 × (∀ i, α(i+1)) and ∀ i, α(i): separating the first element from the tail via cons.

Русский

Существует каноническое эквивалентство между α0 × (∀ i, α(i+1)) и ∀ i, α(i): разделение первого элемента от хвоста через cons.

LaTeX

$$$\\mathrm{consEquiv}$: $\\alpha_0 \\times (\\forall i, \\alpha(\\mathrm{succ}\\, i)) \\simeq (\\forall i, \\alpha i)$$$

Lean4

/-- Concatenating the first element of a tuple with its tail gives back the original tuple -/
@[simp]
theorem cons_self_tail : cons (q 0) (tail q) = q := by
  ext j
  cases j using Fin.cases <;> simp [tail]

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