prod — Mathlib

English

There is a finite enumeration of the product α × β listing all pairs (a,b) with a ∈ toList α and b ∈ toList β.

Русский

Существует конечное перечисление произведения α × β, перечисляющее все пары (a,b) с a ∈ toList α и b ∈ toList β.

LaTeX

$$$ \\mathrm{toList}(\\\\alpha \\times \\\\beta) = \\mathrm{toList}(\\\\alpha) \\times^{\\mathrm{s}} \\mathrm{toList}(\\\\beta). $$$

Lean4

instance prod {β} [FinEnum α] [FinEnum β] : FinEnum (α × β) :=
  ofList (toList α ×ˢ toList β) fun x => by cases x; simp

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