exists_cons — Mathlib

English

Every ListBlank l can be constructed by first choosing a head a and a sublist l' such that l = ListBlank.cons a l'.

Русский

Каждый ListBlank l можно получить, выбрав первый элемент a и подсписок l' так, чтобы l = ListBlank.cons a l'.

LaTeX

$$$\\forall \\Gamma [Inhabited(\\Gamma)],\\ \\exists a,\\exists l',\\ l = \\mathrm{ListBlank.cons}(a,l')$$$

Lean4

/-- The `cons` and `head`/`tail` functions are mutually inverse, unlike in the case of `List` where
this only holds for nonempty lists. -/
theorem exists_cons {Γ} [Inhabited Γ] (l : ListBlank Γ) : ∃ a l', l = ListBlank.cons a l' :=
  ⟨_, _, (ListBlank.cons_head_tail _).symm⟩

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