toFinset_univ

Mathlib.Data.Set.Finite.Basic

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

English

If univ is finite, then its Finset equals Finset.univ.

Русский

Если все множество единиц (univ) конечно, то соответствующий Finset равен Finset.univ.

LaTeX

$$$ h.toFinset = \mathrm{Finset.univ} $$$

Lean4

protected theorem toFinset_univ [Fintype α] (h : (Set.univ : Set α).Finite) : h.toFinset = Finset.univ := by simp

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

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

Разделы

Аффилиация

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