eq_empty_of_isEmpty

Mathlib.Data.Finset.Empty

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

← MathLib Explorer

English

If the underlying type α is empty, then any Finset s of α is the empty set.

Русский

Если базовый тип α пуст, то любой Finset s над α равен пустому множеству.

LaTeX

$$$ [\operatorname{IsEmpty} \alpha] \Rightarrow s = \emptyset $$$

Lean4

/-- A `Finset` for an empty type is empty. -/
theorem eq_empty_of_isEmpty [IsEmpty α] (s : Finset α) : s = ∅ :=
  Finset.eq_empty_of_forall_notMem isEmptyElim

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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