isubtree_cons — Mathlib

English

If ps is augmented with a new head i, then isubtree along M.mk ⟨a,f⟩ equals isubtree along ps with f i.

Русский

Если к ps добавить новый элемент i, то isubtree (⟨_,i⟩ :: ps) (M.mk ⟨a,f⟩) равно isubtree ps (f i).

LaTeX

$$$\\operatorname{isubtree}\\big(\\langle\\_, i\\rangle :: ps\\big)\\big(\\operatorname{M.mk}\\langle a, f\\rangle\\big) = \\operatorname{isubtree}\\ ps\\ (f\\ i)$$$

Lean4

@[simp]
theorem isubtree_cons [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) {a} (f : F.B a → M F) {i : F.B a} :
    isubtree (⟨_, i⟩ :: ps) (M.mk ⟨a, f⟩) = isubtree ps (f i) := by
  simp only [isubtree, dif_pos, isubtree, M.casesOn_mk']; rfl

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