insertRec_empty — Mathlib

English

For any C with H0 on the empty AList, and IH describing the inductive step, insertRec evaluated at the empty list returns H0.

Русский

для любой функции C и базового условия H0 на пустом AList и IH описывающего шаг индукции, значение insertRec на пустом списке равно H0.

LaTeX

$$$ \operatorname{insertRec} \ H0 \ IH \emptyset = H0 $$$

Lean4

@[simp]
theorem insertRec_empty {C : AList β → Sort*} (H0 : C ∅)
    (IH : ∀ (a : α) (b : β a) (l : AList β), a ∉ l → C l → C (l.insert a b)) : @insertRec α β _ C H0 IH ∅ = H0 :=
  by
  change @insertRec α β _ C H0 IH ⟨[], _⟩ = H0
  rw [insertRec]

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