sortedUniv_toFinset — Mathlib

English

For every finite encodable α with decidable equality, converting the sorted universe to a Finset yields the universal Finset over α.

Русский

Для каждого конечного кодируемого типа α с равенством, допускающем решение, преобразование упорядоченного универсума в Finset даёт все элементы α.

LaTeX

$$$(\operatorname{sortedUniv} \alpha).toFinset = \operatorname{Finset.univ}$$$

Lean4

@[simp]
theorem sortedUniv_toFinset (α) [Fintype α] [Encodable α] [DecidableEq α] : (sortedUniv α).toFinset = Finset.univ :=
  Finset.sort_toFinset _ _

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