bidirectionalRec_nil — Mathlib

English

The bidirectionalRec function applied to a singleton list [a] yields the corresponding singleton value.

Русский

Применение bidirectionalRec к одиночному списку [a] даёт соответствующее значение-одиночку.

LaTeX

$$$$ \operatorname{bidirectionalRec} (\text{nil}) (\text{singleton}) (\text{cons\_append}) [a] = \text{singleton } a. $$$$

Lean4

@[simp]
theorem bidirectionalRec_nil {motive : List α → Sort*} (nil : motive []) (singleton : ∀ a : α, motive [a])
    (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) :
    bidirectionalRec nil singleton cons_append [] = nil :=
  bidirectionalRec.eq_1 ..

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