univ_eq_empty

Mathlib.Data.Finset.BooleanAlgebra

URI: https://scilib.ai/kg/mathlib#Finset.univ_eq_empty

English

If α is an empty type, then the universal finite set in α is empty.

Русский

Если α пустого типа, то Finset.univ α = ∅.

LaTeX

$$$(\mathrm{univ} : \mathrm{Finset} \alpha) = \emptyset$$$

Lean4

@[simp]
theorem univ_eq_empty [IsEmpty α] : (univ : Finset α) = ∅ :=
  univ_eq_empty_iff.2 ‹_›

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

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

Разделы

Аффилиация

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