tail_init_eq_init_tail — Mathlib

English

The tail of the initial segment equals the initial segment of the tail: tail(init q) = init(tail q).

Русский

Хвост начального отрезка равен начальному отрезку хвоста: tail(init q) = init(tail q).

LaTeX

$$$\\\\operatorname{tail}(\\\\operatorname{init} q) = \\\\operatorname{init}(\\\\operatorname{tail} q)$$$

Lean4

/-- `tail` and `init` commute. We state this lemma in a non-dependent setting, as otherwise it
would involve a cast to convince Lean that the two types are equal, making it harder to use. -/
theorem tail_init_eq_init_tail {β : Sort*} (q : Fin (n + 2) → β) : tail (init q) = init (tail q) :=
  by
  ext i
  simp [tail, init]

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