ofList — Mathlib

English

Given a List l and a proof H that every x ∈ l, one can construct a finite type on α, i.e., Fintype α.

Русский

Для списка l и доказательства того, что каждый элемент принадлежит l, можно построить конечный тип на α.

LaTeX

$$$\\text{ofList }(l) := Fintype\\ α$$$

Lean4

/-- Construct a proof of `Fintype α` from a universal list -/
def ofList [DecidableEq α] (l : List α) (H : ∀ x : α, x ∈ l) : Fintype α :=
  ⟨l.toFinset, by simpa using H⟩

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