iselect_cons — Mathlib

English

iselect on a cons path reduces to iselect on the tail: iselect (⟨a,i⟩ :: ps) (M.mk ⟨a,f⟩) = iselect ps (f i).

Русский

iselect для конуса пути эквивалентен iselect на хвосте: iselect (⟨a,i⟩ :: ps) (M.mk ⟨a,f⟩) = iselect ps (f i).

LaTeX

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

Lean4

@[simp]
theorem iselect_cons [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) {a} (f : F.B a → M F) {i} :
    iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect ps (f i) := by simp only [iselect, isubtree_cons]

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