recNeNil_singleton — Mathlib

English

In the recNeNil principle, the value on a singleton list [x] is given by the singleton construction.

Русский

В принципе recNeNil значение для списка-одиночки [x] задаётся через конструктор singleton.

LaTeX

$$$$ \operatorname{recNeNil} sequence (\text{singleton}) (\text{cons}) [x] (\text{cons\_ne\_nil } x []) = \text{singleton } x. $$$$

Lean4

@[simp]
theorem recNeNil_singleton {motive : (l : List α) → l ≠ [] → Sort*} (x : α)
    (singleton : ∀ x, motive [x] (cons_ne_nil x []))
    (cons : ∀ x xs h, motive xs h → motive (x :: xs) (cons_ne_nil x xs)) :
    recNeNil singleton cons [x] (cons_ne_nil x []) = singleton x :=
  rfl

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