cons_one — Mathlib

English

For any x and p, the value at index 1 of the tuple cons x p equals the value at index 0 of p: (cons x p)(1) = p(0).

Русский

Для любых x и p значение на позиции 1 в конc x p равно значению на позиции 0 в p: (cons x p)(1) = p(0).

LaTeX

$$$(\\\\mathrm{cons}(x,p))(1) = p(0)$$$

Lean4

@[simp]
theorem cons_one {α : Fin (n + 2) → Sort*} (x : α 0) (p : ∀ i : Fin n.succ, α i.succ) : cons x p 1 = p 0 := by
  rw [← cons_succ x p]; rfl

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