mem_toList — Mathlib

English

Let α be a finite enumerated type. Then every element x of α appears in the enumeration list toList α.

Русский

Пусть α — конечный перечисляемый тип. Тогда любой элемент x ∈ α встречается в списке перечисления toList α.

LaTeX

$$$ \\forall \\alpha\\ (\\\\text{FinEnum }\\\\alpha)\\; \\forall x:\\alpha,\\ x \\in \\mathrm{toList}(\\\\alpha). $$$

Lean4

@[simp]
theorem mem_toList [FinEnum α] (x : α) : x ∈ toList α := by
  simp only [toList, List.mem_map, List.mem_finRange, true_and]; exists equiv x; simp

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