cons_cast_succ — Mathlib

English

Indexing in a cons-shifted series behaves consistently with the base series under appropriate casts.

Русский

Индексация в конс-последовательности соответствует базовой серии при соответствующих преобразованиях индексов.

LaTeX

$$$ (s.cons a h) (.cast (by \\!\\; simp) (.succ i)) = s i $$$

Lean4

theorem cons_cast_succ (s : RelSeries r) (a : α) (h : a ~[r] s.head) (i : Fin (s.length + 1)) :
    (s.cons a h) (.cast (by simp) (.succ i)) = s i :=
  by
  dsimp [cons]
  convert append_apply_right (singleton r a) s h i
  ext1
  dsimp
  omega

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