toFinset_univ

Mathlib.Data.Fintype.Sets

URI: https://scilib.ai/kg/mathlib#Set.toFinset_univ

English

The Finset corresponding to the universe Set.univ is Finset.univ.

Русский

Перечисление всего множества совпадает с Finset.univ.

LaTeX

$$$(\mathrm{Set.univ} : Set\ α).toFinset = \mathrm{Finset.univ}$$$

Lean4

@[simp]
theorem toFinset_univ [Fintype α] [Fintype (Set.univ : Set α)] : (Set.univ : Set α).toFinset = Finset.univ :=
  by
  ext
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru