sum — Mathlib

English

There is a finite enumeration of the sum α ⊕ β listing all elements obtained from inl and inr injections.

Русский

Существует конечное перечисление суммы α ⊕ β, перечисляющее все элементы через инъекции inl и inr.

LaTeX

$$$ \\mathrm{toList}(\\\\alpha \\oplus \\\\beta) = (\\\\mathrm{toList}(\\\\alpha)).map\\\\Sum.inl \\;++\\; (\\\\mathrm{toList}(\\\\beta)).map\\\\Sum.inr. $$$

Lean4

instance sum {β} [FinEnum α] [FinEnum β] : FinEnum (α ⊕ β) :=
  ofList ((toList α).map Sum.inl ++ (toList β).map Sum.inr) fun x => by cases x <;> simp

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