init_update_castSucc — Mathlib

English

Updating at position i.castSucc commutes with taking the beginning: initializing after an update equals updating the beginning after the same index.

Русский

Обновление на позиции i.castSucc commute с операцией инициализации: init (update q i.castSucc y) = update (init q) i y.

LaTeX

$$$\\\\operatorname{init}(\\\\operatorname{update} q i \\\\mathrm{castSucc} \\\\; y) = \\\\operatorname{update}(\\\\operatorname{init} q) i \\\\; y$$$

Lean4

/-- Updating an element and taking the beginning commute. -/
@[simp]
theorem init_update_castSucc : init (update q i.castSucc y) = update (init q) i y :=
  by
  ext j
  by_cases h : j = i
  · rw [h]
    simp [init]
  · simp [init, h, castSucc_inj]

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